A peak occurs at a lease start: amounts are nonnegative and only those
events add reservations. Ends are exclusive; device completion alone cannot
end a lease still extended by a transport read.
385def resourceUsageAt =
386 (lambda unrestricted leases : (family StdList (family ResourceLease)) .
387 (lambda unrestricted domain : Nat .
388 (lambda unrestricted event : Nat .
389 (stdListFold
390 (family ResourceLease)
391 (family ResourceUsage)
392 (lambda unrestricted lease : (family ResourceLease) .
393 (lambda unrestricted total : (family ResourceUsage) .
394 (resourceUsageAdd
395 total
396 (naturalSelect
397 (naturalAnd
398 (naturalEqual domain (resourceLeaseDomain lease))
399 (naturalAnd
400 (naturalLessOrEqual (resourceLeaseBegin lease) event)
401 (naturalLess event (resourceLeaseUntil lease))))
402 (resourceLeaseAmount lease)
403 0))))
404 (constructor ResourceUsage ResourceUsageWithin 0)
405 leases))))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.