388def telemetryDrainArenaCertificate =
389 (lambda unrestricted applicationBytes : Nat .
390 (lambda unrestricted ordinaryCapacity : Nat .
391 (lambda unrestricted reservedCapacity : Nat .
392 (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
393 (lambda unrestricted reserved : (family TelemetryRecordPlan) .
394 (lambda unrestricted bound : Nat .
395 (naturalAnd
396 (publicationStorageCertificateForBody
397 applicationBytes
398 ordinaryCapacity
399 reservedCapacity
400 bound)
401 (naturalAnd
402 (naturalLessOrEqual
403 (telemetryDrainArenaBytes
404 applicationBytes
405 ordinaryCapacity
406 reservedCapacity
407 ordinary
408 reserved
409 bound)
410 captureExtentMaximum)
411 (arenaCertificate
412 (telemetryDrainArenaBytes
413 applicationBytes
414 ordinaryCapacity
415 reservedCapacity
416 ordinary
417 reserved
418 bound)
419 (telemetryDrainResidents
420 applicationBytes
421 ordinaryCapacity
422 reservedCapacity
423 ordinary
424 reserved
425 bound))))))))))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.