3171def coreBoundEqual :
3172 (pi unrestricted index : Nat . (pi unrestricted right : (family CoreTerm) . Nat)) =
3173 (lambda unrestricted index : Nat .
3174 (lambda unrestricted right : (family CoreTerm) .
3175 (eliminate
3176 CoreTerm
3177 (lambda unrestricted term : (family CoreTerm) . Nat)
3178 right
3179 (branch CoreUniverse level . zero)
3180 (branch CoreNatural . zero)
3181 (branch CoreNaturalLiteral value . zero)
3182 (branch CoreBound rightIndex . (naturalEqual index rightIndex))
3183 (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero)
3184 (branch CoreLambda multiplicity domain body ih_domain ih_body . zero)
3185 (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero)
3186 (branch CoreApplication function argument ih_function ih_argument . zero)
3187 (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero)
3188 (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
3189 (branch CoreByte . zero)
3190 (branch CoreByteLiteral value . zero)
3191 (branch CoreBytes . zero)
3192 (branch CoreBytesLiteral value . zero)
3193 (branch CorePrimitiveTerm primitive . zero)
3194 (branch CoreTermSequenceEnd . zero)
3195 (branch CoreTermSequenceNext head tail ih_head ih_tail . zero)
3196 (branch CoreFamilyApplication familyName arguments ih_arguments . zero)
3197 (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero)
3198 (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero)
3199 (branch
3200 CoreEliminator
3201 familyName
3202 motive
3203 scrutinee
3204 branches
3205 ih_motive
3206 ih_scrutinee
3207 ih_branches
3208 .
3209 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.