3211def corePiEqual :
3212 (pi unrestricted multiplicity : (family CoreMultiplicity) .
3213 (pi unrestricted domainEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
3214 (pi unrestricted codomainEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
3215 (pi unrestricted right : (family CoreTerm) . Nat)))) =
3216 (lambda unrestricted multiplicity : (family CoreMultiplicity) .
3217 (lambda unrestricted domainEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
3218 (lambda unrestricted codomainEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
3219 (lambda unrestricted right : (family CoreTerm) .
3220 (eliminate
3221 CoreTerm
3222 (lambda unrestricted term : (family CoreTerm) . Nat)
3223 right
3224 (branch CoreUniverse level . zero)
3225 (branch CoreNatural . zero)
3226 (branch CoreNaturalLiteral value . zero)
3227 (branch CoreBound index . zero)
3228 (branch
3229 CorePi
3230 rightMultiplicity
3231 rightDomain
3232 rightCodomain
3233 ih_rightDomain
3234 ih_rightCodomain
3235 .
3236 (coreNaturalAnd
3237 (multiplicityEqual multiplicity rightMultiplicity)
3238 (coreNaturalAnd (domainEqual rightDomain) (codomainEqual rightCodomain))))
3239 (branch
3240 CoreLambda
3241 rightMultiplicity
3242 rightDomain
3243 rightBody
3244 ih_rightDomain
3245 ih_rightBody
3246 .
3247 zero)
3248 (branch
3249 CoreLet
3250 multiplicity
3251 annotation
3252 value
3253 body
3254 ih_annotation
3255 ih_value
3256 ih_body
3257 .
3258 zero)
3259 (branch CoreApplication function argument ih_function ih_argument . zero)
3260 (branch
3261 CoreNaturalArithmetic
3262 operation
3263 function
3264 argument
3265 ih_function
3266 ih_argument
3267 .
3268 zero)
3269 (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
3270 (branch CoreByte . zero)
3271 (branch CoreByteLiteral value . zero)
3272 (branch CoreBytes . zero)
3273 (branch CoreBytesLiteral value . zero)
3274 (branch CorePrimitiveTerm primitive . zero)
3275 (branch CoreTermSequenceEnd . zero)
3276 (branch CoreTermSequenceNext head tail ih_head ih_tail . zero)
3277 (branch CoreFamilyApplication familyName arguments ih_arguments . zero)
3278 (branch
3279 CoreConstructorApplication
3280 familyName
3281 constructorName
3282 arguments
3283 ih_arguments
3284 .
3285 zero)
3286 (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero)
3287 (branch
3288 CoreEliminator
3289 familyName
3290 motive
3291 scrutinee
3292 branches
3293 ih_motive
3294 ih_scrutinee
3295 ih_branches
3296 .
3297 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.