5466def workShiftCoreTree =
5467 (lambda unrestricted term : (family CoreTerm) .
5468 (eliminate
5469 CoreTerm
5470 (lambda unrestricted current : (family CoreTerm) .
5471 (pi unrestricted depth : Nat .
5472 (pi unrestricted amount : Nat .
5473 (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult)))))
5474 term
5475 (branch
5476 CoreUniverse
5477 coreUniverseLevel
5478 .
5479 (lambda unrestricted depth : Nat .
5480 (lambda unrestricted amount : Nat .
5481 (lambda unrestricted budget : (family NormalizationBudget) .
5482 (coreWorkCharge
5483 coreWorkOne
5484 budget
5485 (lambda unrestricted remaining : (family NormalizationBudget) .
5486 (constructor
5487 CoreWorkResult
5488 CoreWorkCompleted
5489 (constructor CoreTerm CoreUniverse coreUniverseLevel)
5490 remaining)))))))
5491 (branch
5492 CoreNatural
5493 .
5494 (lambda unrestricted depth : Nat .
5495 (lambda unrestricted amount : Nat .
5496 (lambda unrestricted budget : (family NormalizationBudget) .
5497 (coreWorkCharge
5498 coreWorkOne
5499 budget
5500 (lambda unrestricted remaining : (family NormalizationBudget) .
5501 (constructor
5502 CoreWorkResult
5503 CoreWorkCompleted
5504 (constructor CoreTerm CoreNatural)
5505 remaining)))))))
5506 (branch
5507 CoreNaturalLiteral
5508 coreNaturalValue
5509 .
5510 (lambda unrestricted depth : Nat .
5511 (lambda unrestricted amount : Nat .
5512 (lambda unrestricted budget : (family NormalizationBudget) .
5513 (coreWorkCharge
5514 coreWorkOne
5515 budget
5516 (lambda unrestricted remaining : (family NormalizationBudget) .
5517 (constructor
5518 CoreWorkResult
5519 CoreWorkCompleted
5520 (constructor CoreTerm CoreNaturalLiteral coreNaturalValue)
5521 remaining)))))))
5522 (branch
5523 CoreBound
5524 coreBoundIndex
5525 .
5526 (lambda unrestricted depth : Nat .
5527 (lambda unrestricted amount : Nat .
5528 (lambda unrestricted budget : (family NormalizationBudget) .
5529 (coreWorkCharge
5530 coreWorkOne
5531 budget
5532 (lambda unrestricted remaining : (family NormalizationBudget) .
5533 (coreWorkChoose
5534 (nat-less-than coreBoundIndex depth)
5535 (lambda unrestricted force : Nat .
5536 (constructor
5537 CoreWorkResult
5538 CoreWorkCompleted
5539 (constructor CoreTerm CoreBound coreBoundIndex)
5540 remaining))
5541 (lambda unrestricted force : Nat .
5542 (coreWorkChargeNatural
5543 coreBoundIndex
5544 remaining
5545 (lambda unrestricted remaining : (family NormalizationBudget) .
5546 (constructor
5547 CoreWorkResult
5548 CoreWorkCompleted
5549 (shiftCorePart1 coreBoundIndex depth amount)
5550 remaining)))))))))))
5551 (branch
5552 CorePi
5553 corePiMultiplicity
5554 corePiDomain
5555 corePiCodomain
5556 ih_corePiDomain
5557 ih_corePiCodomain
5558 .
5559 (lambda unrestricted depth : Nat .
5560 (lambda unrestricted amount : Nat .
5561 (lambda unrestricted budget : (family NormalizationBudget) .
5562 (coreWorkCharge
5563 coreWorkOne
5564 budget
5565 (lambda unrestricted remaining : (family NormalizationBudget) .
5566 (coreWorkBind
5567 (ih_corePiDomain depth amount remaining)
5568 (lambda unrestricted new_corePiDomain : (family CoreTerm) .
5569 (lambda unrestricted remaining : (family NormalizationBudget) .
5570 (coreWorkBind
5571 (ih_corePiCodomain (succ depth) amount remaining)
5572 (lambda unrestricted new_corePiCodomain : (family CoreTerm) .
5573 (lambda unrestricted remaining : (family NormalizationBudget) .
5574 (constructor
5575 CoreWorkResult
5576 CoreWorkCompleted
5577 (constructor
5578 CoreTerm
5579 CorePi
5580 corePiMultiplicity
5581 new_corePiDomain
5582 new_corePiCodomain)
5583 remaining)))))))))))))
5584 (branch
5585 CoreLambda
5586 coreLambdaMultiplicity
5587 coreLambdaDomain
5588 coreLambdaBody
5589 ih_coreLambdaDomain
5590 ih_coreLambdaBody
5591 .
5592 (lambda unrestricted depth : Nat .
5593 (lambda unrestricted amount : Nat .
5594 (lambda unrestricted budget : (family NormalizationBudget) .
5595 (coreWorkCharge
5596 coreWorkOne
5597 budget
5598 (lambda unrestricted remaining : (family NormalizationBudget) .
5599 (coreWorkBind
5600 (ih_coreLambdaDomain depth amount remaining)
5601 (lambda unrestricted new_coreLambdaDomain : (family CoreTerm) .
5602 (lambda unrestricted remaining : (family NormalizationBudget) .
5603 (coreWorkBind
5604 (ih_coreLambdaBody (succ depth) amount remaining)
5605 (lambda unrestricted new_coreLambdaBody : (family CoreTerm) .
5606 (lambda unrestricted remaining : (family NormalizationBudget) .
5607 (constructor
5608 CoreWorkResult
5609 CoreWorkCompleted
5610 (constructor
5611 CoreTerm
5612 CoreLambda
5613 coreLambdaMultiplicity
5614 new_coreLambdaDomain
5615 new_coreLambdaBody)
5616 remaining)))))))))))))
5617 (branch
5618 CoreLet
5619 coreLetMultiplicity
5620 coreLetAnnotation
5621 coreLetValue
5622 coreLetBody
5623 ih_coreLetAnnotation
5624 ih_coreLetValue
5625 ih_coreLetBody
5626 .
5627 (lambda unrestricted depth : Nat .
5628 (lambda unrestricted amount : Nat .
5629 (lambda unrestricted budget : (family NormalizationBudget) .
5630 (coreWorkCharge
5631 coreWorkOne
5632 budget
5633 (lambda unrestricted remaining : (family NormalizationBudget) .
5634 (coreWorkBind
5635 (ih_coreLetAnnotation depth amount remaining)
5636 (lambda unrestricted new_coreLetAnnotation : (family CoreTerm) .
5637 (lambda unrestricted remaining : (family NormalizationBudget) .
5638 (coreWorkBind
5639 (ih_coreLetValue depth amount remaining)
5640 (lambda unrestricted new_coreLetValue : (family CoreTerm) .
5641 (lambda unrestricted remaining : (family NormalizationBudget) .
5642 (coreWorkBind
5643 (ih_coreLetBody (succ depth) amount remaining)
5644 (lambda unrestricted new_coreLetBody : (family CoreTerm) .
5645 (lambda unrestricted remaining : (family NormalizationBudget) .
5646 (constructor
5647 CoreWorkResult
5648 CoreWorkCompleted
5649 (constructor
5650 CoreTerm
5651 CoreLet
5652 coreLetMultiplicity
5653 new_coreLetAnnotation
5654 new_coreLetValue
5655 new_coreLetBody)
5656 remaining))))))))))))))))
5657 (branch
5658 CoreApplication
5659 coreApplicationFunction
5660 coreApplicationArgument
5661 ih_coreApplicationFunction
5662 ih_coreApplicationArgument
5663 .
5664 (lambda unrestricted depth : Nat .
5665 (lambda unrestricted amount : Nat .
5666 (lambda unrestricted budget : (family NormalizationBudget) .
5667 (coreWorkCharge
5668 coreWorkOne
5669 budget
5670 (lambda unrestricted remaining : (family NormalizationBudget) .
5671 (coreWorkBind
5672 (ih_coreApplicationFunction depth amount remaining)
5673 (lambda unrestricted new_coreApplicationFunction : (family CoreTerm) .
5674 (lambda unrestricted remaining : (family NormalizationBudget) .
5675 (coreWorkBind
5676 (ih_coreApplicationArgument depth amount remaining)
5677 (lambda unrestricted new_coreApplicationArgument : (family CoreTerm) .
5678 (lambda unrestricted remaining : (family NormalizationBudget) .
5679 (constructor
5680 CoreWorkResult
5681 CoreWorkCompleted
5682 (constructor
5683 CoreTerm
5684 CoreApplication
5685 new_coreApplicationFunction
5686 new_coreApplicationArgument)
5687 remaining)))))))))))))
5688 (branch
5689 CoreNaturalArithmetic
5690 coreArithmeticOperation
5691 coreArithmeticLeft
5692 coreArithmeticRight
5693 ih_coreArithmeticLeft
5694 ih_coreArithmeticRight
5695 .
5696 (lambda unrestricted depth : Nat .
5697 (lambda unrestricted amount : Nat .
5698 (lambda unrestricted budget : (family NormalizationBudget) .
5699 (coreWorkCharge
5700 coreWorkOne
5701 budget
5702 (lambda unrestricted remaining : (family NormalizationBudget) .
5703 (coreWorkBind
5704 (ih_coreArithmeticLeft depth amount remaining)
5705 (lambda unrestricted new_coreArithmeticLeft : (family CoreTerm) .
5706 (lambda unrestricted remaining : (family NormalizationBudget) .
5707 (coreWorkBind
5708 (ih_coreArithmeticRight depth amount remaining)
5709 (lambda unrestricted new_coreArithmeticRight : (family CoreTerm) .
5710 (lambda unrestricted remaining : (family NormalizationBudget) .
5711 (constructor
5712 CoreWorkResult
5713 CoreWorkCompleted
5714 (constructor
5715 CoreTerm
5716 CoreNaturalArithmetic
5717 coreArithmeticOperation
5718 new_coreArithmeticLeft
5719 new_coreArithmeticRight)
5720 remaining)))))))))))))
5721 (branch
5722 CoreNaturalSuccessor
5723 coreNaturalPredecessor
5724 ih_coreNaturalPredecessor
5725 .
5726 (lambda unrestricted depth : Nat .
5727 (lambda unrestricted amount : Nat .
5728 (lambda unrestricted budget : (family NormalizationBudget) .
5729 (coreWorkCharge
5730 coreWorkOne
5731 budget
5732 (lambda unrestricted remaining : (family NormalizationBudget) .
5733 (coreWorkBind
5734 (ih_coreNaturalPredecessor depth amount remaining)
5735 (lambda unrestricted new_coreNaturalPredecessor : (family CoreTerm) .
5736 (lambda unrestricted remaining : (family NormalizationBudget) .
5737 (constructor
5738 CoreWorkResult
5739 CoreWorkCompleted
5740 (constructor CoreTerm CoreNaturalSuccessor new_coreNaturalPredecessor)
5741 remaining))))))))))
5742 (branch
5743 CoreByte
5744 .
5745 (lambda unrestricted depth : Nat .
5746 (lambda unrestricted amount : Nat .
5747 (lambda unrestricted budget : (family NormalizationBudget) .
5748 (coreWorkCharge
5749 coreWorkOne
5750 budget
5751 (lambda unrestricted remaining : (family NormalizationBudget) .
5752 (constructor
5753 CoreWorkResult
5754 CoreWorkCompleted
5755 (constructor CoreTerm CoreByte)
5756 remaining)))))))
5757 (branch
5758 CoreByteLiteral
5759 coreByteValue
5760 .
5761 (lambda unrestricted depth : Nat .
5762 (lambda unrestricted amount : Nat .
5763 (lambda unrestricted budget : (family NormalizationBudget) .
5764 (coreWorkCharge
5765 coreWorkOne
5766 budget
5767 (lambda unrestricted remaining : (family NormalizationBudget) .
5768 (constructor
5769 CoreWorkResult
5770 CoreWorkCompleted
5771 (constructor CoreTerm CoreByteLiteral coreByteValue)
5772 remaining)))))))
5773 (branch
5774 CoreBytes
5775 .
5776 (lambda unrestricted depth : Nat .
5777 (lambda unrestricted amount : Nat .
5778 (lambda unrestricted budget : (family NormalizationBudget) .
5779 (coreWorkCharge
5780 coreWorkOne
5781 budget
5782 (lambda unrestricted remaining : (family NormalizationBudget) .
5783 (constructor
5784 CoreWorkResult
5785 CoreWorkCompleted
5786 (constructor CoreTerm CoreBytes)
5787 remaining)))))))
5788 (branch
5789 CoreBytesLiteral
5790 coreBytesValue
5791 .
5792 (lambda unrestricted depth : Nat .
5793 (lambda unrestricted amount : Nat .
5794 (lambda unrestricted budget : (family NormalizationBudget) .
5795 (coreWorkCharge
5796 coreWorkOne
5797 budget
5798 (lambda unrestricted remaining : (family NormalizationBudget) .
5799 (constructor
5800 CoreWorkResult
5801 CoreWorkCompleted
5802 (constructor CoreTerm CoreBytesLiteral coreBytesValue)
5803 remaining)))))))
5804 (branch
5805 CorePrimitiveTerm
5806 corePrimitive
5807 .
5808 (lambda unrestricted depth : Nat .
5809 (lambda unrestricted amount : Nat .
5810 (lambda unrestricted budget : (family NormalizationBudget) .
5811 (coreWorkCharge
5812 coreWorkOne
5813 budget
5814 (lambda unrestricted remaining : (family NormalizationBudget) .
5815 (constructor
5816 CoreWorkResult
5817 CoreWorkCompleted
5818 (constructor CoreTerm CorePrimitiveTerm corePrimitive)
5819 remaining)))))))
5820 (branch
5821 CoreTermSequenceEnd
5822 .
5823 (lambda unrestricted depth : Nat .
5824 (lambda unrestricted amount : Nat .
5825 (lambda unrestricted budget : (family NormalizationBudget) .
5826 (coreWorkCharge
5827 coreWorkOne
5828 budget
5829 (lambda unrestricted remaining : (family NormalizationBudget) .
5830 (constructor
5831 CoreWorkResult
5832 CoreWorkCompleted
5833 (constructor CoreTerm CoreTermSequenceEnd)
5834 remaining)))))))
5835 (branch
5836 CoreTermSequenceNext
5837 coreTermSequenceHead
5838 coreTermSequenceTail
5839 ih_coreTermSequenceHead
5840 ih_coreTermSequenceTail
5841 .
5842 (lambda unrestricted depth : Nat .
5843 (lambda unrestricted amount : Nat .
5844 (lambda unrestricted budget : (family NormalizationBudget) .
5845 (coreWorkCharge
5846 coreWorkOne
5847 budget
5848 (lambda unrestricted remaining : (family NormalizationBudget) .
5849 (coreWorkBind
5850 (ih_coreTermSequenceHead depth amount remaining)
5851 (lambda unrestricted new_coreTermSequenceHead : (family CoreTerm) .
5852 (lambda unrestricted remaining : (family NormalizationBudget) .
5853 (coreWorkBind
5854 (ih_coreTermSequenceTail depth amount remaining)
5855 (lambda unrestricted new_coreTermSequenceTail : (family CoreTerm) .
5856 (lambda unrestricted remaining : (family NormalizationBudget) .
5857 (constructor
5858 CoreWorkResult
5859 CoreWorkCompleted
5860 (constructor
5861 CoreTerm
5862 CoreTermSequenceNext
5863 new_coreTermSequenceHead
5864 new_coreTermSequenceTail)
5865 remaining)))))))))))))
5866 (branch
5867 CoreFamilyApplication
5868 coreFamilyName
5869 coreFamilyArguments
5870 ih_coreFamilyArguments
5871 .
5872 (lambda unrestricted depth : Nat .
5873 (lambda unrestricted amount : Nat .
5874 (lambda unrestricted budget : (family NormalizationBudget) .
5875 (coreWorkCharge
5876 coreWorkOne
5877 budget
5878 (lambda unrestricted remaining : (family NormalizationBudget) .
5879 (coreWorkBind
5880 (ih_coreFamilyArguments depth amount remaining)
5881 (lambda unrestricted new_coreFamilyArguments : (family CoreTerm) .
5882 (lambda unrestricted remaining : (family NormalizationBudget) .
5883 (constructor
5884 CoreWorkResult
5885 CoreWorkCompleted
5886 (constructor
5887 CoreTerm
5888 CoreFamilyApplication
5889 coreFamilyName
5890 new_coreFamilyArguments)
5891 remaining))))))))))
5892 (branch
5893 CoreConstructorApplication
5894 coreConstructorFamilyName
5895 coreConstructorName
5896 coreConstructorArguments
5897 ih_coreConstructorArguments
5898 .
5899 (lambda unrestricted depth : Nat .
5900 (lambda unrestricted amount : Nat .
5901 (lambda unrestricted budget : (family NormalizationBudget) .
5902 (coreWorkCharge
5903 coreWorkOne
5904 budget
5905 (lambda unrestricted remaining : (family NormalizationBudget) .
5906 (coreWorkBind
5907 (ih_coreConstructorArguments depth amount remaining)
5908 (lambda unrestricted new_coreConstructorArguments : (family CoreTerm) .
5909 (lambda unrestricted remaining : (family NormalizationBudget) .
5910 (constructor
5911 CoreWorkResult
5912 CoreWorkCompleted
5913 (constructor
5914 CoreTerm
5915 CoreConstructorApplication
5916 coreConstructorFamilyName
5917 coreConstructorName
5918 new_coreConstructorArguments)
5919 remaining))))))))))
5920 (branch
5921 CoreEliminatorBranch
5922 coreBranchConstructorName
5923 coreBranchBinderCount
5924 coreBranchBody
5925 ih_coreBranchBody
5926 .
5927 (lambda unrestricted depth : Nat .
5928 (lambda unrestricted amount : Nat .
5929 (lambda unrestricted budget : (family NormalizationBudget) .
5930 (coreWorkCharge
5931 coreWorkOne
5932 budget
5933 (lambda unrestricted remaining : (family NormalizationBudget) .
5934 (coreWorkChargeNatural
5935 depth
5936 remaining
5937 (lambda unrestricted remaining : (family NormalizationBudget) .
5938 (coreWorkBind
5939 (ih_coreBranchBody
5940 (naturalAdd depth coreBranchBinderCount)
5941 amount
5942 remaining)
5943 (lambda unrestricted new_coreBranchBody : (family CoreTerm) .
5944 (lambda unrestricted remaining : (family NormalizationBudget) .
5945 (constructor
5946 CoreWorkResult
5947 CoreWorkCompleted
5948 (constructor
5949 CoreTerm
5950 CoreEliminatorBranch
5951 coreBranchConstructorName
5952 coreBranchBinderCount
5953 new_coreBranchBody)
5954 remaining))))))))))))
5955 (branch
5956 CoreEliminator
5957 coreEliminatedFamilyName
5958 coreEliminatorMotive
5959 coreEliminatorScrutinee
5960 coreEliminatorBranches
5961 ih_coreEliminatorMotive
5962 ih_coreEliminatorScrutinee
5963 ih_coreEliminatorBranches
5964 .
5965 (lambda unrestricted depth : Nat .
5966 (lambda unrestricted amount : Nat .
5967 (lambda unrestricted budget : (family NormalizationBudget) .
5968 (coreWorkCharge
5969 coreWorkOne
5970 budget
5971 (lambda unrestricted remaining : (family NormalizationBudget) .
5972 (coreWorkBind
5973 (ih_coreEliminatorMotive depth amount remaining)
5974 (lambda unrestricted new_coreEliminatorMotive : (family CoreTerm) .
5975 (lambda unrestricted remaining : (family NormalizationBudget) .
5976 (coreWorkBind
5977 (ih_coreEliminatorScrutinee depth amount remaining)
5978 (lambda unrestricted new_coreEliminatorScrutinee : (family CoreTerm) .
5979 (lambda unrestricted remaining : (family NormalizationBudget) .
5980 (coreWorkBind
5981 (ih_coreEliminatorBranches depth amount remaining)
5982 (lambda unrestricted new_coreEliminatorBranches : (family CoreTerm) .
5983 (lambda unrestricted remaining : (family NormalizationBudget) .
5984 (constructor
5985 CoreWorkResult
5986 CoreWorkCompleted
5987 (constructor
5988 CoreTerm
5989 CoreEliminator
5990 coreEliminatedFamilyName
5991 new_coreEliminatorMotive
5992 new_coreEliminatorScrutinee
5993 new_coreEliminatorBranches)
5994 remaining))))))))))))))))))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.