3641def coreBytesTypeEqual : (pi unrestricted right : (family CoreTerm) . Nat) =
3642 (lambda unrestricted right : (family CoreTerm) .
3643 (eliminate
3644 CoreTerm
3645 (lambda unrestricted term : (family CoreTerm) . Nat)
3646 right
3647 (branch CoreUniverse level . zero)
3648 (branch CoreNatural . zero)
3649 (branch CoreNaturalLiteral value . zero)
3650 (branch CoreBound index . zero)
3651 (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero)
3652 (branch CoreLambda multiplicity domain body ih_domain ih_body . zero)
3653 (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero)
3654 (branch CoreApplication function argument ih_function ih_argument . zero)
3655 (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero)
3656 (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
3657 (branch CoreByte . zero)
3658 (branch CoreByteLiteral value . zero)
3659 (branch CoreBytes . (succ zero))
3660 (branch CoreBytesLiteral value . zero)
3661 (branch CorePrimitiveTerm primitive . zero)
3662 (branch CoreTermSequenceEnd . zero)
3663 (branch CoreTermSequenceNext head tail ih_head ih_tail . zero)
3664 (branch CoreFamilyApplication familyName arguments ih_arguments . zero)
3665 (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero)
3666 (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero)
3667 (branch
3668 CoreEliminator
3669 familyName
3670 motive
3671 scrutinee
3672 branches
3673 ih_motive
3674 ih_scrutinee
3675 ih_branches
3676 .
3677 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.