4222def coreLetEqual =
4223 (lambda unrestricted multiplicity : (family CoreMultiplicity) .
4224 (lambda unrestricted annotationEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
4225 (lambda unrestricted valueEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
4226 (lambda unrestricted bodyEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
4227 (lambda unrestricted right : (family CoreTerm) .
4228 (eliminate
4229 CoreTerm
4230 (lambda unrestricted current : (family CoreTerm) . Nat)
4231 right
4232 (branch CoreUniverse level . zero)
4233 (branch CoreNatural . zero)
4234 (branch CoreNaturalLiteral value . zero)
4235 (branch CoreBound index . zero)
4236 (branch CorePi m domain codomain ih_domain ih_codomain . zero)
4237 (branch CoreLambda m domain body ih_domain ih_body . zero)
4238 (branch
4239 CoreLet
4240 rightMultiplicity
4241 annotation
4242 value
4243 body
4244 ih_annotation
4245 ih_value
4246 ih_body
4247 .
4248 (coreNaturalAnd
4249 (multiplicityEqual multiplicity rightMultiplicity)
4250 (coreNaturalAnd
4251 (annotationEqual annotation)
4252 (coreNaturalAnd (valueEqual value) (bodyEqual body)))))
4253 (branch CoreApplication function argument ih_function ih_argument . zero)
4254 (branch CoreNaturalArithmetic operation left right ih_left ih_right . zero)
4255 (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
4256 (branch CoreByte . zero)
4257 (branch CoreByteLiteral value . zero)
4258 (branch CoreBytes . zero)
4259 (branch CoreBytesLiteral value . zero)
4260 (branch CorePrimitiveTerm primitive . zero)
4261 (branch CoreTermSequenceEnd . zero)
4262 (branch CoreTermSequenceNext head tail ih_head ih_tail . zero)
4263 (branch CoreFamilyApplication family arguments ih_arguments . zero)
4264 (branch CoreConstructorApplication family constructor arguments ih_arguments . zero)
4265 (branch CoreEliminatorBranch constructor count body ih_body . zero)
4266 (branch
4267 CoreEliminator
4268 family
4269 motive
4270 scrutinee
4271 branches
4272 ih_motive
4273 ih_scrutinee
4274 ih_branches
4275 .
4276 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.