9672def workReserveCoreSequenceProduct =
9673 (lambda unrestricted right : (family CoreTerm) .
9674 (lambda unrestricted left : (family CoreTerm) .
9675 (eliminate
9676 CoreTerm
9677 (lambda unrestricted current : (family CoreTerm) .
9678 (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult)))
9679 left
9680 (branch
9681 CoreUniverse
9682 level
9683 .
9684 (lambda unrestricted budget : (family NormalizationBudget) .
9685 (coreWorkCharge
9686 coreWorkOne
9687 budget
9688 (lambda unrestricted remaining : (family NormalizationBudget) .
9689 (constructor CoreWorkResult CoreWorkCompleted left remaining)))))
9690 (branch
9691 CoreNatural
9692 .
9693 (lambda unrestricted budget : (family NormalizationBudget) .
9694 (coreWorkCharge
9695 coreWorkOne
9696 budget
9697 (lambda unrestricted remaining : (family NormalizationBudget) .
9698 (constructor CoreWorkResult CoreWorkCompleted left remaining)))))
9699 (branch
9700 CoreNaturalLiteral
9701 value
9702 .
9703 (lambda unrestricted budget : (family NormalizationBudget) .
9704 (coreWorkCharge
9705 coreWorkOne
9706 budget
9707 (lambda unrestricted remaining : (family NormalizationBudget) .
9708 (constructor CoreWorkResult CoreWorkCompleted left remaining)))))
9709 (branch
9710 CoreBound
9711 index
9712 .
9713 (lambda unrestricted budget : (family NormalizationBudget) .
9714 (coreWorkCharge
9715 coreWorkOne
9716 budget
9717 (lambda unrestricted remaining : (family NormalizationBudget) .
9718 (constructor CoreWorkResult CoreWorkCompleted left remaining)))))
9719 (branch
9720 CorePi
9721 multiplicity
9722 domain
9723 codomain
9724 ih_domain
9725 ih_codomain
9726 .
9727 (lambda unrestricted budget : (family NormalizationBudget) .
9728 (coreWorkCharge
9729 coreWorkOne
9730 budget
9731 (lambda unrestricted remaining : (family NormalizationBudget) .
9732 (constructor CoreWorkResult CoreWorkCompleted left remaining)))))
9733 (branch
9734 CoreLambda
9735 multiplicity
9736 domain
9737 body
9738 ih_domain
9739 ih_body
9740 .
9741 (lambda unrestricted budget : (family NormalizationBudget) .
9742 (coreWorkCharge
9743 coreWorkOne
9744 budget
9745 (lambda unrestricted remaining : (family NormalizationBudget) .
9746 (constructor CoreWorkResult CoreWorkCompleted left remaining)))))
9747 (branch
9748 CoreLet
9749 multiplicity
9750 annotation
9751 value
9752 body
9753 ih_annotation
9754 ih_value
9755 ih_body
9756 .
9757 (lambda unrestricted budget : (family NormalizationBudget) .
9758 (coreWorkCharge
9759 coreWorkOne
9760 budget
9761 (lambda unrestricted remaining : (family NormalizationBudget) .
9762 (constructor CoreWorkResult CoreWorkCompleted left remaining)))))
9763 (branch
9764 CoreApplication
9765 function
9766 argument
9767 ih_function
9768 ih_argument
9769 .
9770 (lambda unrestricted budget : (family NormalizationBudget) .
9771 (coreWorkCharge
9772 coreWorkOne
9773 budget
9774 (lambda unrestricted remaining : (family NormalizationBudget) .
9775 (constructor CoreWorkResult CoreWorkCompleted left remaining)))))
9776 (branch
9777 CoreNaturalArithmetic
9778 operation
9779 function
9780 argument
9781 ih_function
9782 ih_argument
9783 .
9784 (lambda unrestricted budget : (family NormalizationBudget) .
9785 (coreWorkCharge
9786 coreWorkOne
9787 budget
9788 (lambda unrestricted remaining : (family NormalizationBudget) .
9789 (constructor CoreWorkResult CoreWorkCompleted left remaining)))))
9790 (branch
9791 CoreNaturalSuccessor
9792 predecessor
9793 ih_predecessor
9794 .
9795 (lambda unrestricted budget : (family NormalizationBudget) .
9796 (coreWorkCharge
9797 coreWorkOne
9798 budget
9799 (lambda unrestricted remaining : (family NormalizationBudget) .
9800 (constructor CoreWorkResult CoreWorkCompleted left remaining)))))
9801 (branch
9802 CoreByte
9803 .
9804 (lambda unrestricted budget : (family NormalizationBudget) .
9805 (coreWorkCharge
9806 coreWorkOne
9807 budget
9808 (lambda unrestricted remaining : (family NormalizationBudget) .
9809 (constructor CoreWorkResult CoreWorkCompleted left remaining)))))
9810 (branch
9811 CoreByteLiteral
9812 value
9813 .
9814 (lambda unrestricted budget : (family NormalizationBudget) .
9815 (coreWorkCharge
9816 coreWorkOne
9817 budget
9818 (lambda unrestricted remaining : (family NormalizationBudget) .
9819 (constructor CoreWorkResult CoreWorkCompleted left remaining)))))
9820 (branch
9821 CoreBytes
9822 .
9823 (lambda unrestricted budget : (family NormalizationBudget) .
9824 (coreWorkCharge
9825 coreWorkOne
9826 budget
9827 (lambda unrestricted remaining : (family NormalizationBudget) .
9828 (constructor CoreWorkResult CoreWorkCompleted left remaining)))))
9829 (branch
9830 CoreBytesLiteral
9831 value
9832 .
9833 (lambda unrestricted budget : (family NormalizationBudget) .
9834 (coreWorkCharge
9835 coreWorkOne
9836 budget
9837 (lambda unrestricted remaining : (family NormalizationBudget) .
9838 (constructor CoreWorkResult CoreWorkCompleted left remaining)))))
9839 (branch
9840 CorePrimitiveTerm
9841 primitive
9842 .
9843 (lambda unrestricted budget : (family NormalizationBudget) .
9844 (coreWorkCharge
9845 coreWorkOne
9846 budget
9847 (lambda unrestricted remaining : (family NormalizationBudget) .
9848 (constructor CoreWorkResult CoreWorkCompleted left remaining)))))
9849 (branch
9850 CoreTermSequenceEnd
9851 .
9852 (lambda unrestricted budget : (family NormalizationBudget) .
9853 (coreWorkCharge
9854 coreWorkOne
9855 budget
9856 (lambda unrestricted remaining : (family NormalizationBudget) .
9857 (constructor CoreWorkResult CoreWorkCompleted left remaining)))))
9858 (branch
9859 CoreTermSequenceNext
9860 head
9861 tail
9862 ih_head
9863 ih_tail
9864 .
9865 (lambda unrestricted budget : (family NormalizationBudget) .
9866 (coreWorkCharge
9867 coreWorkOne
9868 budget
9869 (lambda unrestricted remaining : (family NormalizationBudget) .
9870 (coreWorkBind
9871 (ih_tail remaining)
9872 (lambda unrestricted ignored : (family CoreTerm) .
9873 (lambda unrestricted afterTail : (family NormalizationBudget) .
9874 (workCountCoreTermSequence
9875 right
9876 (lambda unrestricted count : Nat .
9877 (lambda unrestricted afterCount : (family NormalizationBudget) .
9878 (constructor CoreWorkResult CoreWorkCompleted left afterCount)))
9879 afterTail))))))))
9880 (branch
9881 CoreFamilyApplication
9882 familyName
9883 arguments
9884 ih_arguments
9885 .
9886 (lambda unrestricted budget : (family NormalizationBudget) .
9887 (coreWorkCharge
9888 coreWorkOne
9889 budget
9890 (lambda unrestricted remaining : (family NormalizationBudget) .
9891 (constructor CoreWorkResult CoreWorkCompleted left remaining)))))
9892 (branch
9893 CoreConstructorApplication
9894 familyName
9895 constructorName
9896 arguments
9897 ih_arguments
9898 .
9899 (lambda unrestricted budget : (family NormalizationBudget) .
9900 (coreWorkCharge
9901 coreWorkOne
9902 budget
9903 (lambda unrestricted remaining : (family NormalizationBudget) .
9904 (constructor CoreWorkResult CoreWorkCompleted left remaining)))))
9905 (branch
9906 CoreEliminatorBranch
9907 constructorName
9908 binderCount
9909 body
9910 ih_body
9911 .
9912 (lambda unrestricted budget : (family NormalizationBudget) .
9913 (coreWorkCharge
9914 coreWorkOne
9915 budget
9916 (lambda unrestricted remaining : (family NormalizationBudget) .
9917 (constructor CoreWorkResult CoreWorkCompleted left remaining)))))
9918 (branch
9919 CoreEliminator
9920 familyName
9921 motive
9922 scrutinee
9923 branches
9924 ih_motive
9925 ih_scrutinee
9926 ih_branches
9927 .
9928 (lambda unrestricted budget : (family NormalizationBudget) .
9929 (coreWorkCharge
9930 coreWorkOne
9931 budget
9932 (lambda unrestricted remaining : (family NormalizationBudget) .
9933 (constructor CoreWorkResult CoreWorkCompleted left 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.