assemble the bits, or overflow
225def specConvert =
226 (lambda unrestricted exponentBits : Nat . (lambda unrestricted fractionBits : Nat . (lambda unrestricted bias : Nat .
227 (lambda unrestricted negative : Nat . (lambda unrestricted digits : Nat . (lambda unrestricted exponent : Nat . (lambda unrestricted exponentNegative : Nat .
228 (nat-eliminate (lambda unrestricted current : Nat . (family SpecResult))
229 (constructor SpecResult SpecBits (nat-multiply negative (specPow2 (nat-add exponentBits fractionBits))))
230 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecResult) .
231 (eliminate SpecFraction (lambda unrestricted current : (family SpecFraction) . (family SpecResult))
232 (specFraction digits exponent exponentNegative)
233 (branch SpecFractionOf numerator denominator .
234 (specAssemble exponentBits fractionBits bias negative
235 (specRound fractionBits bias numerator denominator))))))
236 (specNot (specIsZero digits))))))))))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.