Reserve unary metadata work before invoking legacy index arithmetic.
5445def coreWorkChargeNatural =
5446 (lambda unrestricted amount : Nat .
5447 (lambda unrestricted budget : (family NormalizationBudget) .
5448 (lambda unrestricted continue : (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult)) .
5449 (eliminate
5450 NormalizationChargeResult
5451 (lambda unrestricted current : (family NormalizationChargeResult) .
5452 (family CoreWorkResult))
5453 (chargeNormalizationNatural amount budget)
5454 (branch NormalizationCharged remaining . (continue remaining))
5455 (branch
5456 NormalizationChargeExhausted
5457 remaining
5458 cost
5459 .
5460 (constructor CoreWorkResult CoreWorkExhausted remaining))
5461 (branch
5462 NormalizationChargeInvalid
5463 .
5464 (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.