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 501–530

stdF64FractionNonzero

Full file
501def stdF64FractionNonzero =
502  (lambda unrestricted value : (family ModelFloat64Bits) .
503    (eliminate
504      ModelFloat64Bits
505      (lambda unrestricted current : (family ModelFloat64Bits) . Nat)
506      value
507      (branch
508        ModelFloat64BitsValue
509        b0
510        b1
511        b2
512        b3
513        b4
514        b5
515        b6
516        b7
517        .
518        (stdFlagOr
519          (stdFlagNot (byte-equal (byteAnd b6 (byte 15)) (byte 0)))
520          (stdFlagOr
521            (stdFlagNot (byte-equal b5 (byte 0)))
522            (stdFlagOr
523              (stdFlagNot (byte-equal b4 (byte 0)))
524              (stdFlagOr
525                (stdFlagNot (byte-equal b3 (byte 0)))
526                (stdFlagOr
527                  (stdFlagNot (byte-equal b2 (byte 0)))
528                  (stdFlagOr
529                    (stdFlagNot (byte-equal b1 (byte 0)))
530                    (stdFlagNot (byte-equal b0 (byte 0))))))))))))

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.