Search branch metadata under the shared budget; names are payload-charged.
8762def workFindCoreEliminatorBranch =
8763 (lambda unrestricted constructorName : Bytes .
8764 (lambda unrestricted branches : (family CoreTerm) .
8765 (eliminate
8766 CoreTerm
8767 (lambda unrestricted value : (family CoreTerm) .
8768 (pi unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
8769 (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))))
8770 branches
8771 (branch
8772 CoreUniverse
8773 level
8774 .
8775 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
8776 (lambda unrestricted budget : (family NormalizationBudget) .
8777 (coreWorkCharge
8778 coreWorkOne
8779 budget
8780 (lambda unrestricted remaining : (family NormalizationBudget) .
8781 (continuation
8782 (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)
8783 remaining))))))
8784 (branch
8785 CoreNatural
8786 .
8787 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
8788 (lambda unrestricted budget : (family NormalizationBudget) .
8789 (coreWorkCharge
8790 coreWorkOne
8791 budget
8792 (lambda unrestricted remaining : (family NormalizationBudget) .
8793 (continuation
8794 (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)
8795 remaining))))))
8796 (branch
8797 CoreNaturalLiteral
8798 value
8799 .
8800 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
8801 (lambda unrestricted budget : (family NormalizationBudget) .
8802 (coreWorkCharge
8803 coreWorkOne
8804 budget
8805 (lambda unrestricted remaining : (family NormalizationBudget) .
8806 (continuation
8807 (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)
8808 remaining))))))
8809 (branch
8810 CoreBound
8811 index
8812 .
8813 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
8814 (lambda unrestricted budget : (family NormalizationBudget) .
8815 (coreWorkCharge
8816 coreWorkOne
8817 budget
8818 (lambda unrestricted remaining : (family NormalizationBudget) .
8819 (continuation
8820 (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)
8821 remaining))))))
8822 (branch
8823 CorePi
8824 multiplicity
8825 domain
8826 codomain
8827 ih_domain
8828 ih_codomain
8829 .
8830 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
8831 (lambda unrestricted budget : (family NormalizationBudget) .
8832 (coreWorkCharge
8833 coreWorkOne
8834 budget
8835 (lambda unrestricted remaining : (family NormalizationBudget) .
8836 (continuation
8837 (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)
8838 remaining))))))
8839 (branch
8840 CoreLambda
8841 multiplicity
8842 domain
8843 body
8844 ih_domain
8845 ih_body
8846 .
8847 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
8848 (lambda unrestricted budget : (family NormalizationBudget) .
8849 (coreWorkCharge
8850 coreWorkOne
8851 budget
8852 (lambda unrestricted remaining : (family NormalizationBudget) .
8853 (continuation
8854 (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)
8855 remaining))))))
8856 (branch
8857 CoreLet
8858 multiplicity
8859 annotation
8860 value
8861 body
8862 ih_annotation
8863 ih_value
8864 ih_body
8865 .
8866 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
8867 (lambda unrestricted budget : (family NormalizationBudget) .
8868 (coreWorkCharge
8869 coreWorkOne
8870 budget
8871 (lambda unrestricted remaining : (family NormalizationBudget) .
8872 (continuation
8873 (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)
8874 remaining))))))
8875 (branch
8876 CoreApplication
8877 function
8878 argument
8879 ih_function
8880 ih_argument
8881 .
8882 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
8883 (lambda unrestricted budget : (family NormalizationBudget) .
8884 (coreWorkCharge
8885 coreWorkOne
8886 budget
8887 (lambda unrestricted remaining : (family NormalizationBudget) .
8888 (continuation
8889 (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)
8890 remaining))))))
8891 (branch
8892 CoreNaturalArithmetic
8893 operation
8894 function
8895 argument
8896 ih_function
8897 ih_argument
8898 .
8899 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
8900 (lambda unrestricted budget : (family NormalizationBudget) .
8901 (coreWorkCharge
8902 coreWorkOne
8903 budget
8904 (lambda unrestricted remaining : (family NormalizationBudget) .
8905 (continuation
8906 (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)
8907 remaining))))))
8908 (branch
8909 CoreNaturalSuccessor
8910 predecessor
8911 ih_predecessor
8912 .
8913 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
8914 (lambda unrestricted budget : (family NormalizationBudget) .
8915 (coreWorkCharge
8916 coreWorkOne
8917 budget
8918 (lambda unrestricted remaining : (family NormalizationBudget) .
8919 (continuation
8920 (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)
8921 remaining))))))
8922 (branch
8923 CoreByte
8924 .
8925 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
8926 (lambda unrestricted budget : (family NormalizationBudget) .
8927 (coreWorkCharge
8928 coreWorkOne
8929 budget
8930 (lambda unrestricted remaining : (family NormalizationBudget) .
8931 (continuation
8932 (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)
8933 remaining))))))
8934 (branch
8935 CoreByteLiteral
8936 value
8937 .
8938 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
8939 (lambda unrestricted budget : (family NormalizationBudget) .
8940 (coreWorkCharge
8941 coreWorkOne
8942 budget
8943 (lambda unrestricted remaining : (family NormalizationBudget) .
8944 (continuation
8945 (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)
8946 remaining))))))
8947 (branch
8948 CoreBytes
8949 .
8950 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
8951 (lambda unrestricted budget : (family NormalizationBudget) .
8952 (coreWorkCharge
8953 coreWorkOne
8954 budget
8955 (lambda unrestricted remaining : (family NormalizationBudget) .
8956 (continuation
8957 (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)
8958 remaining))))))
8959 (branch
8960 CoreBytesLiteral
8961 value
8962 .
8963 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
8964 (lambda unrestricted budget : (family NormalizationBudget) .
8965 (coreWorkCharge
8966 coreWorkOne
8967 budget
8968 (lambda unrestricted remaining : (family NormalizationBudget) .
8969 (continuation
8970 (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)
8971 remaining))))))
8972 (branch
8973 CorePrimitiveTerm
8974 primitive
8975 .
8976 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
8977 (lambda unrestricted budget : (family NormalizationBudget) .
8978 (coreWorkCharge
8979 coreWorkOne
8980 budget
8981 (lambda unrestricted remaining : (family NormalizationBudget) .
8982 (continuation
8983 (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)
8984 remaining))))))
8985 (branch
8986 CoreTermSequenceEnd
8987 .
8988 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
8989 (lambda unrestricted budget : (family NormalizationBudget) .
8990 (coreWorkCharge
8991 coreWorkOne
8992 budget
8993 (lambda unrestricted remaining : (family NormalizationBudget) .
8994 (continuation
8995 (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)
8996 remaining))))))
8997 (branch
8998 CoreTermSequenceNext
8999 head
9000 tail
9001 ih_head
9002 ih_tail
9003 .
9004 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
9005 (lambda unrestricted budget : (family NormalizationBudget) .
9006 (coreWorkCharge
9007 coreWorkOne
9008 budget
9009 (lambda unrestricted remaining : (family NormalizationBudget) .
9010 (ih_head
9011 (lambda unrestricted selection : (family CoreEliminatorBranchSelection) .
9012 (lambda unrestricted afterHead : (family NormalizationBudget) .
9013 (eliminate
9014 CoreEliminatorBranchSelection
9015 (lambda unrestricted current : (family CoreEliminatorBranchSelection) .
9016 (family CoreWorkResult))
9017 selection
9018 (branch
9019 CoreEliminatorBranchSelected
9020 count
9021 body
9022 .
9023 (continuation selection afterHead))
9024 (branch CoreEliminatorBranchMissing . (ih_tail continuation afterHead)))))
9025 remaining))))))
9026 (branch
9027 CoreFamilyApplication
9028 familyName
9029 arguments
9030 ih_arguments
9031 .
9032 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
9033 (lambda unrestricted budget : (family NormalizationBudget) .
9034 (coreWorkCharge
9035 coreWorkOne
9036 budget
9037 (lambda unrestricted remaining : (family NormalizationBudget) .
9038 (continuation
9039 (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)
9040 remaining))))))
9041 (branch
9042 CoreConstructorApplication
9043 familyName
9044 nestedConstructorName
9045 arguments
9046 ih_arguments
9047 .
9048 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
9049 (lambda unrestricted budget : (family NormalizationBudget) .
9050 (coreWorkCharge
9051 coreWorkOne
9052 budget
9053 (lambda unrestricted remaining : (family NormalizationBudget) .
9054 (continuation
9055 (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)
9056 remaining))))))
9057 (branch
9058 CoreEliminatorBranch
9059 branchConstructorName
9060 binderCount
9061 body
9062 ih_body
9063 .
9064 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
9065 (lambda unrestricted budget : (family NormalizationBudget) .
9066 (coreWorkCharge
9067 coreWorkOne
9068 budget
9069 (lambda unrestricted remaining : (family NormalizationBudget) .
9070 (coreWorkChargeBytes
9071 constructorName
9072 remaining
9073 (lambda unrestricted afterName : (family NormalizationBudget) .
9074 (coreWorkChargeBytes
9075 branchConstructorName
9076 afterName
9077 (lambda unrestricted afterBranchName : (family NormalizationBudget) .
9078 (coreWorkChoose
9079 (bytes-equal constructorName branchConstructorName)
9080 (lambda unrestricted force : Nat .
9081 (continuation
9082 (constructor
9083 CoreEliminatorBranchSelection
9084 CoreEliminatorBranchSelected
9085 binderCount
9086 body)
9087 afterBranchName))
9088 (lambda unrestricted force : Nat .
9089 (continuation
9090 (constructor
9091 CoreEliminatorBranchSelection
9092 CoreEliminatorBranchMissing)
9093 afterBranchName))))))))))))
9094 (branch
9095 CoreEliminator
9096 familyName
9097 motive
9098 scrutinee
9099 nestedBranches
9100 ih_motive
9101 ih_scrutinee
9102 ih_branches
9103 .
9104 (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) .
9105 (lambda unrestricted budget : (family NormalizationBudget) .
9106 (coreWorkCharge
9107 coreWorkOne
9108 budget
9109 (lambda unrestricted remaining : (family NormalizationBudget) .
9110 (continuation
9111 (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)
9112 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.