Reserve a conservative quadratic allowance for bounded arity arithmetic,
counting, dropping and appending. Substitution consumes its own shared charges.
9937def workReserveCoreEliminatorBookkeeping =
9938 (lambda unrestricted arguments : (family CoreTerm) .
9939 (lambda unrestricted budget : (family NormalizationBudget) .
9940 (nat-eliminate
9941 (lambda unrestricted current : Nat . (family CoreWorkResult))
9942 (constructor CoreWorkResult CoreWorkCompleted arguments budget)
9943 (lambda unrestricted predecessor : Nat .
9944 (lambda unrestricted induction : (family CoreWorkResult) .
9945 (coreWorkBind
9946 induction
9947 (lambda unrestricted ignored : (family CoreTerm) .
9948 (lambda unrestricted remaining : (family NormalizationBudget) .
9949 (workReserveCoreSequenceProduct arguments arguments remaining))))))
9950 (byte-to-nat (byte 16)))))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.