Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 6652–6679

reduceCoreNaturalToByte

Full file
6652def reduceCoreNaturalToByte : (pi unrestricted argument : (family CoreTerm) . (family CoreTerm)) =
6653  (lambda unrestricted argument : (family CoreTerm) .
6654    (eliminate
6655      CoreLiteralInspection
6656      (lambda unrestricted inspection : (family CoreLiteralInspection) . (family CoreTerm))
6657      (inspectCoreLiteral argument)
6658      (branch
6659        CoreNaturalInspected
6660        value
6661        .
6662        (constructor
6663          CoreTerm
6664          CoreByteLiteral
6665          (Compiler.NaturalMagnitudeArithmetic/magnitudeLowByte value)))
6666      (branch
6667        CoreByteInspected
6668        value
6669        .
6670        (corePrimitiveApplication (constructor CorePrimitive CoreNaturalToByte) argument))
6671      (branch
6672        CoreBytesInspected
6673        value
6674        .
6675        (corePrimitiveApplication (constructor CorePrimitive CoreNaturalToByte) argument))
6676      (branch
6677        CoreNotLiteral
6678        .
6679        (corePrimitiveApplication (constructor CorePrimitive CoreNaturalToByte) 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.