199def specAssemble =
200 (lambda unrestricted exponentBits : Nat . (lambda unrestricted fractionBits : Nat . (lambda unrestricted bias : Nat . (lambda unrestricted negative : Nat .
201 (lambda unrestricted rounded : (family SpecRounded) .
202 (eliminate SpecRounded (lambda unrestricted current : (family SpecRounded) . (family SpecResult)) rounded
203 (branch SpecRoundedOf q eOffset subnormal .
204 (nat-eliminate (lambda unrestricted current : Nat . (family SpecResult))
205 (specAssembleNormal exponentBits fractionBits bias negative q eOffset)
206 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecResult) .
207 (constructor SpecResult SpecBits (nat-add (nat-multiply negative (specPow2 (nat-add exponentBits fractionBits))) q))))
208 subnormal))))))))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.