3949def coreFamilyApplicationEqual =
3950 (lambda unrestricted familyName : Bytes .
3951 (lambda unrestricted argumentsEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
3952 (lambda unrestricted right : (family CoreTerm) .
3953 (eliminate
3954 CoreTerm
3955 (lambda unrestricted term : (family CoreTerm) . Nat)
3956 right
3957 (branch CoreUniverse level . zero)
3958 (branch CoreNatural . zero)
3959 (branch CoreNaturalLiteral value . zero)
3960 (branch CoreBound index . zero)
3961 (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero)
3962 (branch CoreLambda multiplicity domain body ih_domain ih_body . zero)
3963 (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero)
3964 (branch CoreApplication function argument ih_function ih_argument . zero)
3965 (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero)
3966 (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
3967 (branch CoreByte . zero)
3968 (branch CoreByteLiteral value . zero)
3969 (branch CoreBytes . zero)
3970 (branch CoreBytesLiteral value . zero)
3971 (branch CorePrimitiveTerm rightPrimitive . zero)
3972 (branch CoreTermSequenceEnd . zero)
3973 (branch CoreTermSequenceNext head tail ih_head ih_tail . zero)
3974 (branch
3975 CoreFamilyApplication
3976 rightFamilyName
3977 arguments
3978 ih_arguments
3979 .
3980 (coreNaturalAnd (coreBytesEqual familyName rightFamilyName) (argumentsEqual arguments)))
3981 (branch
3982 CoreConstructorApplication
3983 rightFamilyName
3984 constructorName
3985 arguments
3986 ih_arguments
3987 .
3988 zero)
3989 (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero)
3990 (branch
3991 CoreEliminator
3992 rightFamilyName
3993 motive
3994 scrutinee
3995 branches
3996 ih_motive
3997 ih_scrutinee
3998 ih_branches
3999 .
4000 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.