Source/Packages

Compiler.NaturalMagnitude

packages/compiler/src/Compiler/NaturalMagnitude.alpha

453 lines33 declarations18.7 KiBSHA-256 8508c0c0b7d6

def · lines 83–102

magnitudeDecimalDigits

Full file
83def magnitudeDecimalDigits =
84  (lambda unrestricted digits : Bytes .
85    (magnitudeAdmitNormalized
86      (app
87        (bytes-eliminate
88          (lambda unrestricted rest : Bytes . (pi unrestricted accumulator : Bytes . Bytes))
89          (lambda unrestricted accumulator : Bytes . accumulator)
90          (lambda unrestricted head : Byte .
91            (lambda unrestricted tail : Bytes .
92              (lambda unrestricted continue : (pi unrestricted accumulator : Bytes . Bytes) .
93                (lambda unrestricted accumulator : Bytes .
94                  (continue
95                    (bytes-cons
96                      (nat-to-byte
97                        (Std.Natural/naturalSaturatingSubtract
98                          (byte-to-nat head)
99                          (byte-to-nat (byte 48))))
100                      accumulator))))))
101          digits)
102        b"")))

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.