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