AlphaGitHub
Source/Packages

Std.Float

packages/foundation/standard/src/Std/Float.alpha

655 lines58 declarations25.1 KiBSHA-256 98de1bd43fa8
Download exact fileView at revisionf5034773ad4bb52133

def · lines 480–499

stdF64ExponentAllOnes

Full file
480def stdF64ExponentAllOnes =
481  (lambda unrestricted value : (family ModelFloat64Bits) .
482    (eliminate
483      ModelFloat64Bits
484      (lambda unrestricted current : (family ModelFloat64Bits) . Nat)
485      value
486      (branch
487        ModelFloat64BitsValue
488        b0
489        b1
490        b2
491        b3
492        b4
493        b5
494        b6
495        b7
496        .
497        (stdFlagAnd
498          (byte-equal (byteAnd b7 (byte 127)) (byte 127))
499          (byte-equal (byteAnd b6 (byte 240)) (byte 240))))))

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.