A natural below 2^24 as its (exact) binary32 word, with naturals that
stay within a machine word, so a program can convert a size at run time
(float32ExactRational's exact rounding needs unbounded naturals and is a
compile-time conversion). The exponent is floor(log2 n); zero is +0.
59def float32SmallNaturalExponent = (lambda unrestricted n : Nat .
60 (nat-eliminate (lambda unrestricted current : Nat . Nat) 0
61 (lambda unrestricted k : Nat . (lambda unrestricted count : Nat .
62 (naturalAdd count (naturalLessOrEqual (naturalPowerOfTwo (succ k)) n)))) 24))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.