IEEE total-order key for finite binary32 values. Negative encodings are
complemented; non-negative encodings have the sign bit set. Unsigned word
comparison then follows numerical order for every admitted finite logit.
43def bobF32OrderKey =
44 (lambda unrestricted value : F32 .
45 (app
46 (lambda unrestricted bits : StdU32 .
47 (nat-eliminate
48 (lambda unrestricted negative : Nat . StdU32)
49 (stdU32Xor bits 0x80000000)
50 (lambda unrestricted predecessor : Nat .
51 (lambda unrestricted induction : StdU32 . (stdU32Not bits)))
52 (stdF32IsNegative value)))
53 (stdF32ToWord32 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.