3601def coreByteLiteralEqual :
3602 (pi unrestricted value : Byte . (pi unrestricted right : (family CoreTerm) . Nat)) =
3603 (lambda unrestricted value : Byte .
3604 (lambda unrestricted right : (family CoreTerm) .
3605 (eliminate
3606 CoreTerm
3607 (lambda unrestricted term : (family CoreTerm) . Nat)
3608 right
3609 (branch CoreUniverse level . zero)
3610 (branch CoreNatural . zero)
3611 (branch CoreNaturalLiteral rightValue . zero)
3612 (branch CoreBound index . zero)
3613 (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero)
3614 (branch CoreLambda multiplicity domain body ih_domain ih_body . zero)
3615 (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero)
3616 (branch CoreApplication function argument ih_function ih_argument . zero)
3617 (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero)
3618 (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
3619 (branch CoreByte . zero)
3620 (branch CoreByteLiteral rightValue . (byte-equal value rightValue))
3621 (branch CoreBytes . zero)
3622 (branch CoreBytesLiteral rightValue . zero)
3623 (branch CorePrimitiveTerm primitive . zero)
3624 (branch CoreTermSequenceEnd . zero)
3625 (branch CoreTermSequenceNext head tail ih_head ih_tail . zero)
3626 (branch CoreFamilyApplication familyName arguments ih_arguments . zero)
3627 (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero)
3628 (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero)
3629 (branch
3630 CoreEliminator
3631 familyName
3632 motive
3633 scrutinee
3634 branches
3635 ih_motive
3636 ih_scrutinee
3637 ih_branches
3638 .
3639 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.