3053def coreUniverseEqual :
3054 (pi unrestricted level : Nat . (pi unrestricted right : (family CoreTerm) . Nat)) =
3055 (lambda unrestricted level : Nat .
3056 (lambda unrestricted right : (family CoreTerm) .
3057 (eliminate
3058 CoreTerm
3059 (lambda unrestricted value : (family CoreTerm) . Nat)
3060 right
3061 (branch CoreUniverse rightLevel . (naturalEqual level rightLevel))
3062 (branch CoreNatural . zero)
3063 (branch CoreNaturalLiteral value . zero)
3064 (branch CoreBound index . zero)
3065 (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero)
3066 (branch CoreLambda multiplicity domain body ih_domain ih_body . zero)
3067 (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero)
3068 (branch CoreApplication function argument ih_function ih_argument . zero)
3069 (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero)
3070 (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
3071 (branch CoreByte . zero)
3072 (branch CoreByteLiteral value . zero)
3073 (branch CoreBytes . zero)
3074 (branch CoreBytesLiteral value . zero)
3075 (branch CorePrimitiveTerm primitive . zero)
3076 (branch CoreTermSequenceEnd . zero)
3077 (branch CoreTermSequenceNext head tail ih_head ih_tail . zero)
3078 (branch CoreFamilyApplication familyName arguments ih_arguments . zero)
3079 (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero)
3080 (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero)
3081 (branch
3082 CoreEliminator
3083 familyName
3084 motive
3085 scrutinee
3086 branches
3087 ih_motive
3088 ih_scrutinee
3089 ih_branches
3090 .
3091 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.