Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 4626–4662

coreTermSequenceCount

Full file
4626def coreTermSequenceCount =
4627  (lambda unrestricted sequence : (family CoreTerm) .
4628    (eliminate
4629      CoreTerm
4630      (lambda unrestricted value : (family CoreTerm) . Nat)
4631      sequence
4632      (branch CoreUniverse level . zero)
4633      (branch CoreNatural . zero)
4634      (branch CoreNaturalLiteral value . zero)
4635      (branch CoreBound index . zero)
4636      (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero)
4637      (branch CoreLambda multiplicity domain body ih_domain ih_body . zero)
4638      (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero)
4639      (branch CoreApplication function argument ih_function ih_argument . zero)
4640      (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero)
4641      (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
4642      (branch CoreByte . zero)
4643      (branch CoreByteLiteral value . zero)
4644      (branch CoreBytes . zero)
4645      (branch CoreBytesLiteral value . zero)
4646      (branch CorePrimitiveTerm primitive . zero)
4647      (branch CoreTermSequenceEnd . zero)
4648      (branch CoreTermSequenceNext head tail ih_head ih_tail . (succ ih_tail))
4649      (branch CoreFamilyApplication familyName arguments ih_arguments . zero)
4650      (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero)
4651      (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero)
4652      (branch
4653        CoreEliminator
4654        familyName
4655        motive
4656        scrutinee
4657        branches
4658        ih_motive
4659        ih_scrutinee
4660        ih_branches
4661        .
4662        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.