An I32 as the nearest binary32 (ties to even): always defined; zero is +0.
269def stdI32ToF32 : (pi unrestricted value : (family StdI32) . (family InferenceFloat32)) =
270 (lambda unrestricted value : (family StdI32) .
271 (app
272 (lambda unrestricted bits : Nat .
273 (app
274 (lambda unrestricted negative : Nat .
275 (app
276 (lambda unrestricted magnitude : Nat .
277 (nat-eliminate
278 (lambda unrestricted current : Nat . (family InferenceFloat32))
279 stdF32Zero
280 (lambda unrestricted magnitudePredecessor : Nat .
281 (lambda unrestricted magnitudeInduction : (family InferenceFloat32) .
282 (stdFloatF32FromMagnitude negative magnitude)))
283 magnitude))
284 (nat-eliminate
285 (lambda unrestricted current : Nat . Nat)
286 bits
287 (lambda unrestricted signPredecessor : Nat .
288 (lambda unrestricted signInduction : Nat . (nat-subtract 4294967296 bits)))
289 negative)))
290 (naturalIsZero (nat-less-than bits 2147483648))))
291 (modelWord32ToNatural (stdI32ToWord value))))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.