192def specAssembleNormal =
193 (lambda unrestricted exponentBits : Nat . (lambda unrestricted fractionBits : Nat . (lambda unrestricted bias : Nat . (lambda unrestricted negative : Nat .
194 (lambda unrestricted q : Nat . (lambda unrestricted eOffset : Nat .
195 (specAssembleField exponentBits fractionBits negative
196 (specSelect (specEqual q (specPow2 (nat-add fractionBits 1))) (nat-divide q 2) q)
197 (nat-subtract (nat-add (specSelect (specEqual q (specPow2 (nat-add fractionBits 1))) (nat-add eOffset 1) eOffset) bias) specOffset))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.