AlphaGitHub
Source/Packages

Compiler.NaturalMagnitude

packages/compiler/src/Compiler/NaturalMagnitude.alpha

453 lines33 declarations18.7 KiBSHA-256 8508c0c0b7d6
Download exact fileView at revisionf5034773ad4bb52133

def · lines 287–294

magnitudeCanonicalValid

Full file
287def magnitudeCanonicalValid =
288  (lambda unrestricted digits : Bytes .
289    (eliminate
290      NaturalMagnitudeResult
291      (lambda unrestricted result : (family NaturalMagnitudeResult) . Nat)
292      (magnitudeDecodeCanonical digits)
293      (branch NaturalMagnitudeAccepted valid . (succ zero))
294      (branch NaturalMagnitudeRejected failure . zero)))

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.