264def rpLeaseTotal =
265 (lambda unrestricted domain : Nat .
266 (lambda unrestricted leases : (family StdResult (family NativePhysicalMemoryFailure) (family StdList (family ResourceLease))) .
267 (eliminate
268 StdResult
269 (lambda unrestricted r : (family StdResult (family NativePhysicalMemoryFailure) (family StdList (family ResourceLease))) .
270 Nat)
271 leases
272 (branch StdFailure error . 0)
273 (branch
274 StdSuccess
275 values
276 .
277 (stdListFold
278 (family ResourceLease)
279 Nat
280 (lambda unrestricted lease : (family ResourceLease) .
281 (lambda unrestricted total : Nat .
282 (naturalAdd
283 (naturalSelect
284 (naturalEqual domain (resourceLeaseDomain lease))
285 (resourceLeaseAmount lease)
286 0)
287 total)))
288 0
289 values)))))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.