187def specAssembleNormal =
188 (lambda unrestricted exponentBits : Nat . (lambda unrestricted fractionBits : Nat . (lambda unrestricted bias : Nat . (lambda unrestricted negative : Nat .
189 (lambda unrestricted q : Nat . (lambda unrestricted eOffset : Nat .
190 (specAssembleField exponentBits fractionBits negative
191 (specSelect (specEqual q (specPow2 (nat-add fractionBits 1))) (nat-divide q 2) q)
192 (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.