3812def corePrimitiveTermEqual :
3813 (pi unrestricted primitive : (family CorePrimitive) .
3814 (pi unrestricted right : (family CoreTerm) . Nat)) =
3815 (lambda unrestricted primitive : (family CorePrimitive) .
3816 (lambda unrestricted right : (family CoreTerm) .
3817 (eliminate
3818 CoreTerm
3819 (lambda unrestricted term : (family CoreTerm) . Nat)
3820 right
3821 (branch CoreUniverse level . zero)
3822 (branch CoreNatural . zero)
3823 (branch CoreNaturalLiteral value . zero)
3824 (branch CoreBound index . zero)
3825 (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero)
3826 (branch CoreLambda multiplicity domain body ih_domain ih_body . zero)
3827 (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero)
3828 (branch CoreApplication function argument ih_function ih_argument . zero)
3829 (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero)
3830 (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
3831 (branch CoreByte . zero)
3832 (branch CoreByteLiteral value . zero)
3833 (branch CoreBytes . zero)
3834 (branch CoreBytesLiteral value . zero)
3835 (branch
3836 CorePrimitiveTerm
3837 rightPrimitive
3838 .
3839 (naturalEqual (corePrimitiveCode primitive) (corePrimitiveCode rightPrimitive)))
3840 (branch CoreTermSequenceEnd . zero)
3841 (branch CoreTermSequenceNext head tail ih_head ih_tail . zero)
3842 (branch CoreFamilyApplication familyName arguments ih_arguments . zero)
3843 (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero)
3844 (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero)
3845 (branch
3846 CoreEliminator
3847 familyName
3848 motive
3849 scrutinee
3850 branches
3851 ih_motive
3852 ih_scrutinee
3853 ih_branches
3854 .
3855 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.