The checkpoint validator examines representations, not floating-point
arithmetic: exponent 255 means infinity or NaN in either IEEE binary32 or
bfloat16. This is the same predicate used by the native host routine below.
24def finiteF32Bits =
25 (lambda unrestricted bits : Nat .
26 (naturalSelect
27 (naturalEqual
28 (naturalModuloUnchecked (naturalDivideUnchecked bits 8388608) 256)
29 255)
30 0 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.