181def specAssembleField =
182 (lambda unrestricted exponentBits : Nat . (lambda unrestricted fractionBits : Nat . (lambda unrestricted negative : Nat .
183 (lambda unrestricted q : Nat . (lambda unrestricted expField : Nat .
184 (nat-eliminate (lambda unrestricted current : Nat . (family SpecResult))
185 (constructor SpecResult SpecBits
186 (nat-add (nat-multiply negative (specPow2 (nat-add exponentBits fractionBits)))
187 (nat-add (nat-multiply expField (specPow2 fractionBits)) (nat-subtract q (specPow2 fractionBits)))))
188 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecResult) .
189 (constructor SpecResult SpecOverflow)))
190 (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.