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 437–453

magnitudePredecessorChecked

Full file
437def magnitudePredecessorChecked =
438  (lambda unrestricted digits : Bytes .
439    (eliminate
440      NaturalMagnitudeResult
441      (lambda unrestricted current : (family NaturalMagnitudeResult) .
442        (family NaturalMagnitudeResult))
443      (magnitudeDecodeCanonical digits)
444      (branch
445        NaturalMagnitudeAccepted
446        value
447        .
448        (magnitudeAdmitNormalized (magnitudePredecessor value)))
449      (branch
450        NaturalMagnitudeRejected
451        error
452        .
453        (constructor NaturalMagnitudeResult NaturalMagnitudeRejected error))))

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.