3299def coreLambdaEqual :
3300 (pi unrestricted multiplicity : (family CoreMultiplicity) .
3301 (pi unrestricted domainEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
3302 (pi unrestricted bodyEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
3303 (pi unrestricted right : (family CoreTerm) . Nat)))) =
3304 (lambda unrestricted multiplicity : (family CoreMultiplicity) .
3305 (lambda unrestricted domainEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
3306 (lambda unrestricted bodyEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
3307 (lambda unrestricted right : (family CoreTerm) .
3308 (eliminate
3309 CoreTerm
3310 (lambda unrestricted term : (family CoreTerm) . Nat)
3311 right
3312 (branch CoreUniverse level . zero)
3313 (branch CoreNatural . zero)
3314 (branch CoreNaturalLiteral value . zero)
3315 (branch CoreBound index . zero)
3316 (branch
3317 CorePi
3318 rightMultiplicity
3319 rightDomain
3320 rightCodomain
3321 ih_rightDomain
3322 ih_rightCodomain
3323 .
3324 zero)
3325 (branch
3326 CoreLambda
3327 rightMultiplicity
3328 rightDomain
3329 rightBody
3330 ih_rightDomain
3331 ih_rightBody
3332 .
3333 (coreNaturalAnd
3334 (multiplicityEqual multiplicity rightMultiplicity)
3335 (coreNaturalAnd (domainEqual rightDomain) (bodyEqual rightBody))))
3336 (branch
3337 CoreLet
3338 multiplicity
3339 annotation
3340 value
3341 body
3342 ih_annotation
3343 ih_value
3344 ih_body
3345 .
3346 zero)
3347 (branch CoreApplication function argument ih_function ih_argument . zero)
3348 (branch
3349 CoreNaturalArithmetic
3350 operation
3351 function
3352 argument
3353 ih_function
3354 ih_argument
3355 .
3356 zero)
3357 (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
3358 (branch CoreByte . zero)
3359 (branch CoreByteLiteral value . zero)
3360 (branch CoreBytes . zero)
3361 (branch CoreBytesLiteral value . zero)
3362 (branch CorePrimitiveTerm primitive . zero)
3363 (branch CoreTermSequenceEnd . zero)
3364 (branch CoreTermSequenceNext head tail ih_head ih_tail . zero)
3365 (branch CoreFamilyApplication familyName arguments ih_arguments . zero)
3366 (branch
3367 CoreConstructorApplication
3368 familyName
3369 constructorName
3370 arguments
3371 ih_arguments
3372 .
3373 zero)
3374 (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero)
3375 (branch
3376 CoreEliminator
3377 familyName
3378 motive
3379 scrutinee
3380 branches
3381 ih_motive
3382 ih_scrutinee
3383 ih_branches
3384 .
3385 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.