3895def coreTermSequenceNextEqual =
3896 (lambda unrestricted headEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
3897 (lambda unrestricted tailEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
3898 (lambda unrestricted right : (family CoreTerm) .
3899 (eliminate
3900 CoreTerm
3901 (lambda unrestricted term : (family CoreTerm) . Nat)
3902 right
3903 (branch CoreUniverse level . zero)
3904 (branch CoreNatural . zero)
3905 (branch CoreNaturalLiteral value . zero)
3906 (branch CoreBound index . zero)
3907 (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero)
3908 (branch CoreLambda multiplicity domain body ih_domain ih_body . zero)
3909 (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero)
3910 (branch CoreApplication function argument ih_function ih_argument . zero)
3911 (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero)
3912 (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
3913 (branch CoreByte . zero)
3914 (branch CoreByteLiteral value . zero)
3915 (branch CoreBytes . zero)
3916 (branch CoreBytesLiteral value . zero)
3917 (branch CorePrimitiveTerm rightPrimitive . zero)
3918 (branch CoreTermSequenceEnd . zero)
3919 (branch
3920 CoreTermSequenceNext
3921 head
3922 tail
3923 ih_head
3924 ih_tail
3925 .
3926 (coreNaturalAnd (headEqual head) (tailEqual tail)))
3927 (branch CoreFamilyApplication familyName arguments ih_arguments . zero)
3928 (branch
3929 CoreConstructorApplication
3930 familyName
3931 constructorName
3932 arguments
3933 ih_arguments
3934 .
3935 zero)
3936 (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero)
3937 (branch
3938 CoreEliminator
3939 familyName
3940 motive
3941 scrutinee
3942 branches
3943 ih_motive
3944 ih_scrutinee
3945 ih_branches
3946 .
3947 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.