AlphaGitHub
Source/Packages

Compiler.NaturalMagnitudeArithmetic

packages/compiler/src/Compiler/NaturalMagnitudeArithmetic.alpha

592 lines29 declarations28.9 KiBSHA-256 9c904be71be4
Download exact fileView at revisionf5034773ad4bb52133

def · lines 102–109

magnitudeFromNatural

Full file
102def magnitudeFromNatural =
103  (lambda unrestricted value : Nat .
104    (nat-eliminate
105      (lambda unrestricted count : Nat . Bytes)
106      b""
107      (lambda unrestricted predecessor : Nat .
108        (lambda unrestricted digits : Bytes . (magnitudeSuccessorDigits digits)))
109      value))

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.