176def specAssembleField =
177 (lambda unrestricted exponentBits : Nat . (lambda unrestricted fractionBits : Nat . (lambda unrestricted negative : Nat .
178 (lambda unrestricted q : Nat . (lambda unrestricted expField : Nat .
179 (nat-eliminate (lambda unrestricted current : Nat . (family SpecResult))
180 (constructor SpecResult SpecBits
181 (nat-add (nat-multiply negative (specPow2 (nat-add exponentBits fractionBits)))
182 (nat-add (nat-multiply expField (specPow2 fractionBits)) (nat-subtract q (specPow2 fractionBits)))))
183 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecResult) .
184 (constructor SpecResult SpecOverflow)))
185 (nat-less-than (nat-subtract (specPow2 exponentBits) 2) expField)))))))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.