Source/Packages

Compiler.NormalizationBudget

packages/compiler/src/Compiler/NormalizationBudget.alpha

775 lines53 declarations32.9 KiBSHA-256 582a37dd050a

def · lines 62–74

normalizationCostDecimalText

Full file
Magnitudes are decimal digits in little-endian order. Conversion visits at most ten admitted digits, never the represented natural value.
62def normalizationCostDecimalText =
63  (lambda unrestricted digits : Bytes .
64    (bytes-eliminate
65      (lambda unrestricted current : Bytes . Bytes)
66      b""
67      (lambda unrestricted head : Byte .
68        (lambda unrestricted tail : Bytes .
69          (lambda unrestricted induction : Bytes .
70            (bytes-append
71              induction
72              (bytes
73                (nat-to-byte (Std.Natural/naturalAdd (byte-to-nat head) (byte-to-nat (byte 48)))))))))
74      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.