395def chargeNormalizationBudget =
396 (lambda unrestricted amount : (family ModelWord32) .
397 (lambda unrestricted budget : (family NormalizationBudget) .
398 (app
399 (nat-eliminate
400 (lambda unrestricted one : Nat .
401 (pi unrestricted force : Nat . (family NormalizationChargeResult)))
402 (lambda unrestricted force : Nat . (chargeNormalizationBudgetGeneral amount budget))
403 (lambda unrestricted predecessor : Nat .
404 (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationChargeResult)) .
405 (lambda unrestricted force : Nat . (chargeNormalizationBudgetOne budget))))
406 (bytes-equal (Std.Word/stdU32EncodeLE amount) (bytes 1 0 0 0)))
407 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.