343def chargeNormalizationBudgetOneValid =
344 (lambda unrestricted budget : (family NormalizationBudget) .
345 (eliminate
346 NormalizationBudget
347 (lambda unrestricted current : (family NormalizationBudget) .
348 (family NormalizationChargeResult))
349 budget
350 (branch
351 NormalizationBudgetValue
352 limit
353 remaining
354 used
355 .
356 (app
357 (nat-eliminate
358 (lambda unrestricted empty : Nat .
359 (pi unrestricted force : Nat . (family NormalizationChargeResult)))
360 (lambda unrestricted force : Nat .
361 (constructor
362 NormalizationChargeResult
363 NormalizationCharged
364 (constructor
365 NormalizationBudget
366 NormalizationBudgetValue
367 limit
368 (normalizationWordPredecessor remaining)
369 (Std.Word/stdU32AddWrapping used normalizationWordOne))))
370 (lambda unrestricted predecessor : Nat .
371 (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationChargeResult)) .
372 (lambda unrestricted force : Nat .
373 (constructor
374 NormalizationChargeResult
375 NormalizationChargeExhausted
376 budget
377 normalizationWordOne))))
378 (Std.Word/stdU32IsZero remaining))
379 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.