Bounded integer ordering for already-admitted finite binary32 words.
Positive encodings increase with magnitude; negative encodings reverse
that order. This total order places -0 below +0, useful for extrema. It
does not specify NaN comparison and is not IEEE's signed-zero equality.
Unlike an exact rational reference comparator, it needs no large integers
or float instruction, so both the checker and native code can execute it.
141def dataFloat32FiniteWordBelow =
142 (lambda unrestricted left : Nat . (lambda unrestricted right : Nat .
143 (let unrestricted leftSign = (nat-divide left 2147483648) in
144 (let unrestricted rightSign = (nat-divide right 2147483648) in
145 (naturalSelect (naturalEqual leftSign rightSign)
146 (naturalSelect leftSign (nat-less-than right left) (nat-less-than left right))
147 leftSign)))))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.