a value in [lo, hi] / d less the value of `word` (a positive binary32
below 2^24, exponent field at most 150): the binary32 nearest the
difference, its sign set when the word is the larger; zero when the
interval reaches the word's value (the difference is below its width
139def float32ExactRemainder =
140 (lambda unrestricted lo : Nat .
141 (lambda unrestricted hi : Nat .
142 (lambda unrestricted d : Nat .
143 (lambda unrestricted word : Nat .
144 (let unrestricted shift = (specPow2 (nat-subtract 150 (modelExponent word))) in
145 (let unrestricted value = (nat-multiply (nat-add (modelFraction word) modelPow2Twenty3) d) in
146 (let unrestricted low = (nat-multiply lo shift) in
147 (let unrestricted high = (nat-multiply hi shift) in
148 (let unrestricted scale = (nat-multiply d shift) in
149 (specSelect (nat-less-than value low)
150 (float32ExactBetween (nat-subtract low value) scale (nat-subtract high value) scale)
151 (specSelect (nat-less-than high value)
152 (nat-add modelPow2Thirty1 (float32ExactBetween (nat-subtract value high) scale (nat-subtract value low) scale))
153 0)))))))))))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.