Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 7719–7730

workInspectCoreBytes

Full file
7719def workInspectCoreBytes =
7720  (lambda unrestricted value : (family CoreTerm) .
7721    (lambda unrestricted selected : (pi unrestricted payload : Bytes . (family CoreWorkResult)) .
7722      (lambda unrestricted fallback : (pi unrestricted force : Nat . (family CoreWorkResult)) .
7723        (eliminate
7724          CoreLiteralInspection
7725          (lambda unrestricted current : (family CoreLiteralInspection) . (family CoreWorkResult))
7726          (inspectCoreLiteral value)
7727          (branch CoreNaturalInspected payload . (fallback zero))
7728          (branch CoreByteInspected payload . (fallback zero))
7729          (branch CoreBytesInspected payload . (selected payload))
7730          (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.