Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 7732–7743

workInspectCoreNatural

Full file
7732def workInspectCoreNatural =
7733  (lambda unrestricted value : (family CoreTerm) .
7734    (lambda unrestricted selected : (pi unrestricted payload : Bytes . (family CoreWorkResult)) .
7735      (lambda unrestricted fallback : (pi unrestricted force : Nat . (family CoreWorkResult)) .
7736        (eliminate
7737          CoreLiteralInspection
7738          (lambda unrestricted current : (family CoreLiteralInspection) . (family CoreWorkResult))
7739          (inspectCoreLiteral value)
7740          (branch CoreNaturalInspected payload . (selected payload))
7741          (branch CoreByteInspected payload . (fallback zero))
7742          (branch CoreBytesInspected payload . (fallback zero))
7743          (branch CoreNotLiteral . (fallback 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.