A sequence of checked unit charges; exhaustion retains the last valid budget.
This bounds the natural cursor by the remaining budget, including U32_MAX.
741def chargeNormalizationNatural =
742 (lambda unrestricted target : Nat .
743 (lambda unrestricted budget : (family NormalizationBudget) .
744 (app
745 (nat-eliminate
746 (lambda unrestricted valid : Nat .
747 (pi unrestricted force : Nat . (family NormalizationChargeResult)))
748 (lambda unrestricted force : Nat .
749 (constructor NormalizationChargeResult NormalizationChargeInvalid))
750 (lambda unrestricted predecessor : Nat .
751 (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationChargeResult)) .
752 (lambda unrestricted force : Nat .
753 (eliminate
754 NormalizationBudget
755 (lambda unrestricted current : (family NormalizationBudget) .
756 (family NormalizationChargeResult))
757 budget
758 (branch
759 NormalizationBudgetValue
760 limit
761 remaining
762 used
763 .
764 (finishNormalizationNatural
765 target
766 (iterateNormalizationNatural
767 (Std.Word/stdU32EncodeLE remaining)
768 (stepNormalizationNatural target)
769 (constructor
770 NormalizationNaturalState
771 NormalizationNaturalActive
772 zero
773 budget))))))))
774 (normalizationBudgetValid budget))
775 zero)))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.