4072def coreEliminatorBranchEqual =
4073 (lambda unrestricted constructorName : Bytes .
4074 (lambda unrestricted binderCount : Nat .
4075 (lambda unrestricted bodyEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
4076 (lambda unrestricted right : (family CoreTerm) .
4077 (eliminate
4078 CoreTerm
4079 (lambda unrestricted value : (family CoreTerm) . Nat)
4080 right
4081 (branch CoreUniverse level . zero)
4082 (branch CoreNatural . zero)
4083 (branch CoreNaturalLiteral value . zero)
4084 (branch CoreBound index . zero)
4085 (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero)
4086 (branch CoreLambda multiplicity domain body ih_domain ih_body . zero)
4087 (branch
4088 CoreLet
4089 multiplicity
4090 annotation
4091 value
4092 body
4093 ih_annotation
4094 ih_value
4095 ih_body
4096 .
4097 zero)
4098 (branch CoreApplication function argument ih_function ih_argument . zero)
4099 (branch
4100 CoreNaturalArithmetic
4101 operation
4102 function
4103 argument
4104 ih_function
4105 ih_argument
4106 .
4107 zero)
4108 (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
4109 (branch CoreByte . zero)
4110 (branch CoreByteLiteral value . zero)
4111 (branch CoreBytes . zero)
4112 (branch CoreBytesLiteral value . zero)
4113 (branch CorePrimitiveTerm primitive . zero)
4114 (branch CoreTermSequenceEnd . zero)
4115 (branch CoreTermSequenceNext head tail ih_head ih_tail . zero)
4116 (branch CoreFamilyApplication familyName arguments ih_arguments . zero)
4117 (branch
4118 CoreConstructorApplication
4119 familyName
4120 rightConstructorName
4121 arguments
4122 ih_arguments
4123 .
4124 zero)
4125 (branch
4126 CoreEliminatorBranch
4127 rightConstructorName
4128 rightBinderCount
4129 rightBody
4130 ih_rightBody
4131 .
4132 (coreNaturalAnd
4133 (coreNaturalAnd
4134 (coreBytesEqual constructorName rightConstructorName)
4135 (naturalEqual binderCount rightBinderCount))
4136 (bodyEqual rightBody)))
4137 (branch
4138 CoreEliminator
4139 familyName
4140 motive
4141 scrutinee
4142 branches
4143 ih_motive
4144 ih_scrutinee
4145 ih_branches
4146 .
4147 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.