I2FP.F32.S32: the 32-bit word read as a signed integer, rounded to binary32
230def modelF32FromSigned32 =
231 (lambda unrestricted word : Nat .
232 (specSelect (nat-less-than word modelPow2Thirty1)
233 (modelRoundBits 0 word 1)
234 (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.