Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 3719–3810

corePrimitiveCode

Full file
3719def corePrimitiveCode : (pi unrestricted primitive : (family CorePrimitive) . Nat) =
3720  (lambda unrestricted primitive : (family CorePrimitive) .
3721    (eliminate
3722      CorePrimitive
3723      (lambda unrestricted value : (family CorePrimitive) . Nat)
3724      primitive
3725      (branch CoreByteEqual . zero)
3726      (branch CoreByteLess . (succ zero))
3727      (branch CoreNaturalLess . (succ (succ zero)))
3728      (branch CoreNaturalToByte . (succ (succ (succ zero))))
3729      (branch CoreByteToNatural . (succ (succ (succ (succ zero)))))
3730      (branch CoreBytesAppend . (succ (succ (succ (succ (succ zero))))))
3731      (branch CoreBytesCons . (succ (succ (succ (succ (succ (succ zero)))))))
3732      (branch CoreBytesLength . (succ (succ (succ (succ (succ (succ (succ zero))))))))
3733      (branch CoreNaturalEliminate . (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))
3734      (branch
3735        CoreBytesEliminate
3736        .
3737        (succ (succ (succ (succ (succ (succ (succ (succ (succ zero))))))))))
3738      (branch
3739        CoreBytesEqual
3740        .
3741        (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))))
3742      (branch CoreFileEffect . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0)))
3743      (branch CoreEffects . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0)))
3744      (branch CoreComputation . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3745      (branch CoreReturn . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3746      (branch CoreBind . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3747      (branch CoreReadFile . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3748      (branch CoreWriteFile . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3749      (branch
3750        CoreLinuxOpenNode
3751        .
3752        (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3753      (branch
3754        CoreLinuxCloseNode
3755        .
3756        (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3757      (branch
3758        CoreLinuxIoctl
3759        .
3760        (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3761      (branch
3762        CoreLinuxMmap
3763        .
3764        (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3765      (branch
3766        CoreLinuxMunmap
3767        .
3768        (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3769      (branch CoreBytesSetIndex . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3770      (branch CoreBytesIndexNonzero . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3771      (branch
3772        CoreBytesSetFreeIndex
3773        .
3774        (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3775      (branch
3776        CoreBytesBuilderType
3777        .
3778        (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3779      (branch
3780        CoreBytesBuilderEmpty
3781        .
3782        (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3783      (branch
3784        CoreBytesBuilderChunk
3785        .
3786        (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3787      (branch
3788        CoreBytesBuilderAppend
3789        .
3790        (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3791      (branch
3792        CoreBytesBuilderBuild
3793        .
3794        (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3795      (branch
3796        CoreRuntimeImageV4Build
3797        .
3798        (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3799      (branch
3800        CoreBytesHead
3801        .
3802        (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3803      (branch
3804        CoreBytesTail
3805        .
3806        (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
3807      (branch
3808        CoreBytesChecksum
3809        .
3810        (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))))

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.