3522def coreNaturalSuccessorEqual :
3523 (pi unrestricted predecessorEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
3524 (pi unrestricted right : (family CoreTerm) . Nat)) =
3525 (lambda unrestricted predecessorEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
3526 (lambda unrestricted right : (family CoreTerm) .
3527 (eliminate
3528 CoreTerm
3529 (lambda unrestricted term : (family CoreTerm) . Nat)
3530 right
3531 (branch CoreUniverse level . zero)
3532 (branch CoreNatural . zero)
3533 (branch CoreNaturalLiteral value . zero)
3534 (branch CoreBound index . zero)
3535 (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero)
3536 (branch CoreLambda multiplicity domain body ih_domain ih_body . zero)
3537 (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero)
3538 (branch CoreApplication function argument ih_function ih_argument . zero)
3539 (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero)
3540 (branch CoreNaturalSuccessor predecessor ih_predecessor . (predecessorEqual predecessor))
3541 (branch CoreByte . zero)
3542 (branch CoreByteLiteral value . zero)
3543 (branch CoreBytes . zero)
3544 (branch CoreBytesLiteral value . zero)
3545 (branch CorePrimitiveTerm primitive . zero)
3546 (branch CoreTermSequenceEnd . zero)
3547 (branch CoreTermSequenceNext head tail ih_head ih_tail . zero)
3548 (branch CoreFamilyApplication familyName arguments ih_arguments . zero)
3549 (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero)
3550 (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero)
3551 (branch
3552 CoreEliminator
3553 familyName
3554 motive
3555 scrutinee
3556 branches
3557 ih_motive
3558 ih_scrutinee
3559 ih_branches
3560 .
3561 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.