3679def coreBytesLiteralEqual :
3680 (pi unrestricted value : Bytes . (pi unrestricted right : (family CoreTerm) . Nat)) =
3681 (lambda unrestricted value : Bytes .
3682 (lambda unrestricted right : (family CoreTerm) .
3683 (eliminate
3684 CoreTerm
3685 (lambda unrestricted term : (family CoreTerm) . Nat)
3686 right
3687 (branch CoreUniverse level . zero)
3688 (branch CoreNatural . zero)
3689 (branch CoreNaturalLiteral rightValue . zero)
3690 (branch CoreBound index . zero)
3691 (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero)
3692 (branch CoreLambda multiplicity domain body ih_domain ih_body . zero)
3693 (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero)
3694 (branch CoreApplication function argument ih_function ih_argument . zero)
3695 (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero)
3696 (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
3697 (branch CoreByte . zero)
3698 (branch CoreByteLiteral rightValue . zero)
3699 (branch CoreBytes . zero)
3700 (branch CoreBytesLiteral rightValue . (coreBytesEqual value rightValue))
3701 (branch CorePrimitiveTerm primitive . zero)
3702 (branch CoreTermSequenceEnd . zero)
3703 (branch CoreTermSequenceNext head tail ih_head ih_tail . zero)
3704 (branch CoreFamilyApplication familyName arguments ih_arguments . zero)
3705 (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero)
3706 (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero)
3707 (branch
3708 CoreEliminator
3709 familyName
3710 motive
3711 scrutinee
3712 branches
3713 ih_motive
3714 ih_scrutinee
3715 ih_branches
3716 .
3717 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.