4149def coreEliminatorEqual =
4150 (lambda unrestricted familyName : Bytes .
4151 (lambda unrestricted motiveEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
4152 (lambda unrestricted scrutineeEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
4153 (lambda unrestricted branchesEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
4154 (lambda unrestricted right : (family CoreTerm) .
4155 (eliminate
4156 CoreTerm
4157 (lambda unrestricted value : (family CoreTerm) . Nat)
4158 right
4159 (branch CoreUniverse level . zero)
4160 (branch CoreNatural . zero)
4161 (branch CoreNaturalLiteral value . zero)
4162 (branch CoreBound index . zero)
4163 (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero)
4164 (branch CoreLambda multiplicity domain body ih_domain ih_body . zero)
4165 (branch
4166 CoreLet
4167 multiplicity
4168 annotation
4169 value
4170 body
4171 ih_annotation
4172 ih_value
4173 ih_body
4174 .
4175 zero)
4176 (branch CoreApplication function argument ih_function ih_argument . zero)
4177 (branch
4178 CoreNaturalArithmetic
4179 operation
4180 function
4181 argument
4182 ih_function
4183 ih_argument
4184 .
4185 zero)
4186 (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
4187 (branch CoreByte . zero)
4188 (branch CoreByteLiteral value . zero)
4189 (branch CoreBytes . zero)
4190 (branch CoreBytesLiteral value . zero)
4191 (branch CorePrimitiveTerm primitive . zero)
4192 (branch CoreTermSequenceEnd . zero)
4193 (branch CoreTermSequenceNext head tail ih_head ih_tail . zero)
4194 (branch CoreFamilyApplication rightFamilyName arguments ih_arguments . zero)
4195 (branch
4196 CoreConstructorApplication
4197 rightFamilyName
4198 constructorName
4199 arguments
4200 ih_arguments
4201 .
4202 zero)
4203 (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero)
4204 (branch
4205 CoreEliminator
4206 rightFamilyName
4207 motive
4208 scrutinee
4209 branches
4210 ih_motive
4211 ih_scrutinee
4212 ih_branches
4213 .
4214 (coreNaturalAnd
4215 (coreNaturalAnd
4216 (coreNaturalAnd
4217 (coreBytesEqual familyName rightFamilyName)
4218 (motiveEqual motive))
4219 (scrutineeEqual scrutinee))
4220 (branchesEqual branches)))))))))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.