3857def coreTermSequenceEndEqual =
3858 (lambda unrestricted right : (family CoreTerm) .
3859 (eliminate
3860 CoreTerm
3861 (lambda unrestricted term : (family CoreTerm) . Nat)
3862 right
3863 (branch CoreUniverse level . zero)
3864 (branch CoreNatural . zero)
3865 (branch CoreNaturalLiteral value . zero)
3866 (branch CoreBound index . zero)
3867 (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero)
3868 (branch CoreLambda multiplicity domain body ih_domain ih_body . zero)
3869 (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero)
3870 (branch CoreApplication function argument ih_function ih_argument . zero)
3871 (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero)
3872 (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
3873 (branch CoreByte . zero)
3874 (branch CoreByteLiteral value . zero)
3875 (branch CoreBytes . zero)
3876 (branch CoreBytesLiteral value . zero)
3877 (branch CorePrimitiveTerm rightPrimitive . zero)
3878 (branch CoreTermSequenceEnd . (succ zero))
3879 (branch CoreTermSequenceNext head tail ih_head ih_tail . zero)
3880 (branch CoreFamilyApplication familyName arguments ih_arguments . zero)
3881 (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero)
3882 (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero)
3883 (branch
3884 CoreEliminator
3885 familyName
3886 motive
3887 scrutinee
3888 branches
3889 ih_motive
3890 ih_scrutinee
3891 ih_branches
3892 .
3893 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.