F64 classification: sign = byte 7 high bit; exponent = byte 7 low seven bits
and byte 6 high four bits (eleven bits); fraction = byte 6 low four bits and
bytes 5..0.
428def stdF64IsNegative =
429 (lambda unrestricted value : (family ModelFloat64Bits) .
430 (eliminate
431 ModelFloat64Bits
432 (lambda unrestricted current : (family ModelFloat64Bits) . Nat)
433 value
434 (branch
435 ModelFloat64BitsValue
436 b0
437 b1
438 b2
439 b3
440 b4
441 b5
442 b6
443 b7
444 .
445 (stdFlagNot (byte-less-than b7 (byte 128))))))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.