3452def coreArithmeticEqual =
3453 (lambda unrestricted operation : (family CoreNaturalOperation) .
3454 (lambda unrestricted functionEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
3455 (lambda unrestricted argumentEqual : (pi unrestricted right : (family CoreTerm) . Nat) .
3456 (lambda unrestricted right : (family CoreTerm) .
3457 (eliminate
3458 CoreTerm
3459 (lambda unrestricted term : (family CoreTerm) . Nat)
3460 right
3461 (branch CoreUniverse level . zero)
3462 (branch CoreNatural . zero)
3463 (branch CoreNaturalLiteral value . zero)
3464 (branch CoreBound index . zero)
3465 (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero)
3466 (branch CoreLambda multiplicity domain body ih_domain ih_body . zero)
3467 (branch
3468 CoreLet
3469 multiplicity
3470 annotation
3471 value
3472 body
3473 ih_annotation
3474 ih_value
3475 ih_body
3476 .
3477 zero)
3478 (branch CoreApplication function argument ih_function ih_argument . zero)
3479 (branch
3480 CoreNaturalArithmetic
3481 rightOperation
3482 rightFunction
3483 rightArgument
3484 ih_rightFunction
3485 ih_rightArgument
3486 .
3487 (coreNaturalAnd
3488 (byte-equal
3489 (coreNaturalOperationCode operation)
3490 (coreNaturalOperationCode rightOperation))
3491 (coreNaturalAnd (functionEqual rightFunction) (argumentEqual rightArgument))))
3492 (branch CoreNaturalSuccessor predecessor ih_predecessor . zero)
3493 (branch CoreByte . zero)
3494 (branch CoreByteLiteral value . zero)
3495 (branch CoreBytes . zero)
3496 (branch CoreBytesLiteral value . zero)
3497 (branch CorePrimitiveTerm primitive . zero)
3498 (branch CoreTermSequenceEnd . zero)
3499 (branch CoreTermSequenceNext head tail ih_head ih_tail . zero)
3500 (branch CoreFamilyApplication familyName arguments ih_arguments . zero)
3501 (branch
3502 CoreConstructorApplication
3503 familyName
3504 constructorName
3505 arguments
3506 ih_arguments
3507 .
3508 zero)
3509 (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero)
3510 (branch
3511 CoreEliminator
3512 familyName
3513 motive
3514 scrutinee
3515 branches
3516 ih_motive
3517 ih_scrutinee
3518 ih_branches
3519 .
3520 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.