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 6681–6708

reduceCoreByteToNatural

Full file
6681def reduceCoreByteToNatural : (pi unrestricted argument : (family CoreTerm) . (family CoreTerm)) =
6682  (lambda unrestricted argument : (family CoreTerm) .
6683    (eliminate
6684      CoreLiteralInspection
6685      (lambda unrestricted inspection : (family CoreLiteralInspection) . (family CoreTerm))
6686      (inspectCoreLiteral argument)
6687      (branch
6688        CoreNaturalInspected
6689        value
6690        .
6691        (corePrimitiveApplication (constructor CorePrimitive CoreByteToNatural) argument))
6692      (branch
6693        CoreByteInspected
6694        value
6695        .
6696        (constructor
6697          CoreTerm
6698          CoreNaturalLiteral
6699          (Compiler.NaturalMagnitudeArithmetic/magnitudeFromNatural (byte-to-nat value))))
6700      (branch
6701        CoreBytesInspected
6702        value
6703        .
6704        (corePrimitiveApplication (constructor CorePrimitive CoreByteToNatural) argument))
6705      (branch
6706        CoreNotLiteral
6707        .
6708        (corePrimitiveApplication (constructor CorePrimitive CoreByteToNatural) argument))))

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.