Source/Packages

Compiler.NaturalMagnitudeArithmetic

packages/compiler/src/Compiler/NaturalMagnitudeArithmetic.alpha

592 lines29 declarations28.9 KiBSHA-256 9c904be71be4

def · lines 116–131

magnitudeLowByte

Full file
116def magnitudeLowByte =
117  (lambda unrestricted digits : Bytes .
118    (bytes-eliminate
119      (lambda unrestricted rest : Bytes . Byte)
120      (byte 0)
121      (lambda unrestricted head : Byte .
122        (lambda unrestricted tail : Bytes .
123          (lambda unrestricted continue : Byte .
124            (nat-to-byte
125              (Std.Natural/naturalAdd
126                (byte-to-nat head)
127                (Std.Natural/naturalAdd
128                  (byte-to-nat (magnitudeByteDouble continue))
129                  (byte-to-nat
130                    (magnitudeByteDouble (magnitudeByteDouble (magnitudeByteDouble continue))))))))))
131      digits))

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.