The nearest binary32 to a positive integer magnitude: exactly when it has at most
24 significant bits, otherwise its low bits rounded away (a carry to 2^24 moves
the exponent).
242def stdFloatF32FromMagnitude =
243 (lambda unrestricted negative : Nat .
244 (lambda unrestricted magnitude : Nat .
245 (app
246 (lambda unrestricted exponent : Nat .
247 (nat-eliminate
248 (lambda unrestricted current : Nat . (family InferenceFloat32))
249 (app
250 (lambda unrestricted rounded : Nat .
251 (nat-eliminate
252 (lambda unrestricted current : Nat . (family InferenceFloat32))
253 (stdFloatF32Assemble negative exponent rounded)
254 (lambda unrestricted carryPredecessor : Nat .
255 (lambda unrestricted carryInduction : (family InferenceFloat32) .
256 (stdFloatF32Assemble negative (succ exponent) 8388608)))
257 (naturalEqual rounded 16777216)))
258 (stdFloatRoundedShift magnitude (nat-subtract exponent 23)))
259 (lambda unrestricted exactPredecessor : Nat .
260 (lambda unrestricted exactInduction : (family InferenceFloat32) .
261 (stdFloatF32Assemble
262 negative
263 exponent
264 (nat-multiply magnitude (naturalPowerOfTwo (nat-subtract 23 exponent))))))
265 (nat-less-than exponent 24)))
266 (stdFloatFloorLog2 magnitude))))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.