212def chargeValidNormalizationBudget =
213 (lambda unrestricted amount : (family ModelWord32) .
214 (lambda unrestricted budget : (family NormalizationBudget) .
215 (eliminate
216 NormalizationBudget
217 (lambda unrestricted current : (family NormalizationBudget) .
218 (family NormalizationChargeResult))
219 budget
220 (branch
221 NormalizationBudgetValue
222 limit
223 remaining
224 used
225 .
226 (app
227 (nat-eliminate
228 (lambda unrestricted insufficient : Nat .
229 (pi unrestricted force : Nat . (family NormalizationChargeResult)))
230 (lambda unrestricted force : Nat .
231 (constructor
232 NormalizationChargeResult
233 NormalizationCharged
234 (constructor
235 NormalizationBudget
236 NormalizationBudgetValue
237 limit
238 (Std.Word/stdU32SubtractWrapping remaining amount)
239 (Std.Word/stdU32AddWrapping used amount))))
240 (lambda unrestricted predecessor : Nat .
241 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NormalizationChargeResult)) .
242 (lambda unrestricted force : Nat .
243 (constructor
244 NormalizationChargeResult
245 NormalizationChargeExhausted
246 budget
247 amount))))
248 (Std.Word/stdU32LessThan remaining amount))
249 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.