AlphaGitHub
Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796
Download exact fileView at revisionf5034773ad4bb52133

def · lines 12350–12365

inferCoreNaturalMagnitude

Full file
12350def inferCoreNaturalMagnitude =
12351  (lambda unrestricted digits : Bytes .
12352    (eliminate
12353      NaturalMagnitudeResult
12354      (lambda unrestricted result : (family NaturalMagnitudeResult) . (family CoreInferenceResult))
12355      (Compiler.NaturalMagnitude/magnitudeDecodeCanonical digits)
12356      (branch
12357        NaturalMagnitudeAccepted
12358        valid
12359        .
12360        (constructor CoreInferenceResult CoreInferred (constructor CoreTerm CoreNatural)))
12361      (branch
12362        NaturalMagnitudeRejected
12363        failure
12364        .
12365        (constructor CoreInferenceResult CoreInferenceFailed coreNaturalMagnitudeFailureCode))))

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.