4002def coreConstructorApplicationEqual =
4003 (lambda unrestricted familyName : Bytes .
4004 (lambda unrestricted constructorName : Bytes .
4005 (lambda unrestricted argumentsEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
4006 (lambda unrestricted right : (family CoreTerm) .
4007 (eliminate
4008 CoreTerm
4009 (lambda unrestricted value : (family CoreTerm) . Nat)
4010 right
4011 (branch CoreUniverse level . zero)
4012 (branch CoreNatural . zero)
4013 (branch CoreNaturalLiteral value . zero)
4014 (branch CoreBound index . zero)
4015 (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero)
4016 (branch CoreLambda multiplicity domain body ih_domain ih_body . zero)
4017 (branch
4018 CoreLet
4019 multiplicity
4020 annotation
4021 value
4022 body
4023 ih_annotation
4024 ih_value
4025 ih_body
4026 .
4027 zero)
4028 (branch CoreApplication function argument ih_function ih_argument . zero)
4029 (branch
4030 CoreNaturalArithmetic
4031 operation
4032 function
4033 argument
4034 ih_function
4035 ih_argument
4036 .
4037 zero)
4038 (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
4039 (branch CoreByte . zero)
4040 (branch CoreByteLiteral value . zero)
4041 (branch CoreBytes . zero)
4042 (branch CoreBytesLiteral value . zero)
4043 (branch CorePrimitiveTerm primitive . zero)
4044 (branch CoreTermSequenceEnd . zero)
4045 (branch CoreTermSequenceNext head tail ih_head ih_tail . zero)
4046 (branch CoreFamilyApplication rightFamilyName arguments ih_arguments . zero)
4047 (branch
4048 CoreConstructorApplication
4049 rightFamilyName
4050 rightConstructorName
4051 arguments
4052 ih_arguments
4053 .
4054 (coreNaturalAnd
4055 (coreNaturalAnd
4056 (coreBytesEqual familyName rightFamilyName)
4057 (coreBytesEqual constructorName rightConstructorName))
4058 (argumentsEqual arguments)))
4059 (branch CoreEliminatorBranch rightConstructorName binderCount body ih_body . zero)
4060 (branch
4061 CoreEliminator
4062 rightFamilyName
4063 motive
4064 scrutinee
4065 branches
4066 ih_motive
4067 ih_scrutinee
4068 ih_branches
4069 .
4070 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.