3387def coreApplicationEqual :
3388 (pi unrestricted functionEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
3389 (pi unrestricted argumentEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
3390 (pi unrestricted right : (family CoreTerm) . Nat))) =
3391 (lambda unrestricted functionEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
3392 (lambda unrestricted argumentEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
3393 (lambda unrestricted right : (family CoreTerm) .
3394 (eliminate
3395 CoreTerm
3396 (lambda unrestricted term : (family CoreTerm) . Nat)
3397 right
3398 (branch CoreUniverse level . zero)
3399 (branch CoreNatural . zero)
3400 (branch CoreNaturalLiteral value . zero)
3401 (branch CoreBound index . zero)
3402 (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero)
3403 (branch CoreLambda multiplicity domain body ih_domain ih_body . zero)
3404 (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero)
3405 (branch
3406 CoreApplication
3407 rightFunction
3408 rightArgument
3409 ih_rightFunction
3410 ih_rightArgument
3411 .
3412 (coreNaturalAnd (functionEqual rightFunction) (argumentEqual rightArgument)))
3413 (branch
3414 CoreNaturalArithmetic
3415 operation
3416 rightFunction
3417 rightArgument
3418 ih_rightFunction
3419 ih_rightArgument
3420 .
3421 zero)
3422 (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
3423 (branch CoreByte . zero)
3424 (branch CoreByteLiteral value . zero)
3425 (branch CoreBytes . zero)
3426 (branch CoreBytesLiteral value . zero)
3427 (branch CorePrimitiveTerm primitive . zero)
3428 (branch CoreTermSequenceEnd . zero)
3429 (branch CoreTermSequenceNext head tail ih_head ih_tail . zero)
3430 (branch CoreFamilyApplication familyName arguments ih_arguments . zero)
3431 (branch
3432 CoreConstructorApplication
3433 familyName
3434 constructorName
3435 arguments
3436 ih_arguments
3437 .
3438 zero)
3439 (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero)
3440 (branch
3441 CoreEliminator
3442 familyName
3443 motive
3444 scrutinee
3445 branches
3446 ih_motive
3447 ih_scrutinee
3448 ih_branches
3449 .
3450 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.