3563def coreByteEqual : (pi unrestricted right : (family CoreTerm) . Nat) =
3564 (lambda unrestricted right : (family CoreTerm) .
3565 (eliminate
3566 CoreTerm
3567 (lambda unrestricted term : (family CoreTerm) . Nat)
3568 right
3569 (branch CoreUniverse level . zero)
3570 (branch CoreNatural . zero)
3571 (branch CoreNaturalLiteral value . zero)
3572 (branch CoreBound index . zero)
3573 (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero)
3574 (branch CoreLambda multiplicity domain body ih_domain ih_body . zero)
3575 (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero)
3576 (branch CoreApplication function argument ih_function ih_argument . zero)
3577 (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero)
3578 (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
3579 (branch CoreByte . (succ zero))
3580 (branch CoreByteLiteral value . zero)
3581 (branch CoreBytes . zero)
3582 (branch CoreBytesLiteral value . zero)
3583 (branch CorePrimitiveTerm primitive . zero)
3584 (branch CoreTermSequenceEnd . zero)
3585 (branch CoreTermSequenceNext head tail ih_head ih_tail . zero)
3586 (branch CoreFamilyApplication familyName arguments ih_arguments . zero)
3587 (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero)
3588 (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero)
3589 (branch
3590 CoreEliminator
3591 familyName
3592 motive
3593 scrutinee
3594 branches
3595 ih_motive
3596 ih_scrutinee
3597 ih_branches
3598 .
3599 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.