Each natural transition costs at least one unit. Reject an unaffordable
count before iteration; substitutions then debit the shared remaining budget.
7601def workNaturalEliminate =
7602 (lambda unrestricted digits : Bytes .
7603 (lambda unrestricted zeroCase : (family CoreTerm) .
7604 (lambda unrestricted successorCase : (family CoreTerm) .
7605 (lambda unrestricted budget : (family NormalizationBudget) .
7606 (eliminate
7607 NormalizationCostResult
7608 (lambda unrestricted current : (family NormalizationCostResult) .
7609 (family CoreWorkResult))
7610 (Compiler.NormalizationBudget/normalizationCostFromMagnitude digits)
7611 (branch
7612 NormalizationCostWord
7613 cost
7614 .
7615 (coreWorkCharge
7616 cost
7617 budget
7618 (lambda unrestricted remaining : (family NormalizationBudget) .
7619 (finishCoreNaturalWork
7620 (iterateCoreNaturalWork
7621 digits
7622 (stepCoreNaturalWork successorCase)
7623 (constructor
7624 CoreNaturalWorkState
7625 CoreNaturalWorkActive
7626 b""
7627 zeroCase
7628 remaining))))))
7629 (branch
7630 NormalizationCostTooLarge
7631 .
7632 (constructor CoreWorkResult CoreWorkExhausted budget))
7633 (branch
7634 NormalizationCostInvalid
7635 .
7636 (constructor CoreWorkResult CoreWorkExhausted budget)))))))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.