3131def coreNaturalLiteralEqual :
3132 (pi unrestricted value : Bytes . (pi unrestricted right : (family CoreTerm) . Nat)) =
3133 (lambda unrestricted value : Bytes .
3134 (lambda unrestricted right : (family CoreTerm) .
3135 (eliminate
3136 CoreTerm
3137 (lambda unrestricted term : (family CoreTerm) . Nat)
3138 right
3139 (branch CoreUniverse level . zero)
3140 (branch CoreNatural . zero)
3141 (branch CoreNaturalLiteral rightValue . (bytes-equal value rightValue))
3142 (branch CoreBound index . zero)
3143 (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero)
3144 (branch CoreLambda multiplicity domain body ih_domain ih_body . zero)
3145 (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero)
3146 (branch CoreApplication function argument ih_function ih_argument . zero)
3147 (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero)
3148 (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
3149 (branch CoreByte . zero)
3150 (branch CoreByteLiteral rightValue . zero)
3151 (branch CoreBytes . zero)
3152 (branch CoreBytesLiteral rightValue . zero)
3153 (branch CorePrimitiveTerm primitive . zero)
3154 (branch CoreTermSequenceEnd . zero)
3155 (branch CoreTermSequenceNext head tail ih_head ih_tail . zero)
3156 (branch CoreFamilyApplication familyName arguments ih_arguments . zero)
3157 (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero)
3158 (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero)
3159 (branch
3160 CoreEliminator
3161 familyName
3162 motive
3163 scrutinee
3164 branches
3165 ih_motive
3166 ih_scrutinee
3167 ih_branches
3168 .
3169 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.