3093def coreNaturalEqual : (pi unrestricted right : (family CoreTerm) . Nat) =
3094 (lambda unrestricted right : (family CoreTerm) .
3095 (eliminate
3096 CoreTerm
3097 (lambda unrestricted value : (family CoreTerm) . Nat)
3098 right
3099 (branch CoreUniverse level . zero)
3100 (branch CoreNatural . (succ zero))
3101 (branch CoreNaturalLiteral value . zero)
3102 (branch CoreBound index . zero)
3103 (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero)
3104 (branch CoreLambda multiplicity domain body ih_domain ih_body . zero)
3105 (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero)
3106 (branch CoreApplication function argument ih_function ih_argument . zero)
3107 (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero)
3108 (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
3109 (branch CoreByte . zero)
3110 (branch CoreByteLiteral value . zero)
3111 (branch CoreBytes . zero)
3112 (branch CoreBytesLiteral value . zero)
3113 (branch CorePrimitiveTerm primitive . zero)
3114 (branch CoreTermSequenceEnd . zero)
3115 (branch CoreTermSequenceNext head tail ih_head ih_tail . zero)
3116 (branch CoreFamilyApplication familyName arguments ih_arguments . zero)
3117 (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero)
3118 (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero)
3119 (branch
3120 CoreEliminator
3121 familyName
3122 motive
3123 scrutinee
3124 branches
3125 ih_motive
3126 ih_scrutinee
3127 ih_branches
3128 .
3129 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.