I2FP.F32.S32: the 32-bit word read as a signed integer, rounded to binary32
336def modelF32FromSigned32 =
337 (lambda unrestricted word : Nat .
338 (specSelect (nat-less-than word modelPow2Thirty1)
339 (modelRoundBits 0 word 1)
340 (modelRoundBits 1 (nat-subtract (nat-multiply 2 modelPow2Thirty1) word) 1)))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.