418def telemetryPolicyArenaCertificate =
419 (lambda unrestricted applicationBytes : Nat .
420 (lambda unrestricted ordinaryCapacity : Nat .
421 (lambda unrestricted reservedCapacity : Nat .
422 (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
423 (lambda unrestricted reserved : (family TelemetryRecordPlan) .
424 (lambda unrestricted bound : Nat .
425 (naturalAnd
426 (telemetryDrainArenaCertificate
427 applicationBytes
428 ordinaryCapacity
429 reservedCapacity
430 ordinary
431 reserved
432 bound)
433 (naturalAnd
434 (naturalLessOrEqual
435 (telemetryPolicyArenaBytes
436 applicationBytes
437 ordinaryCapacity
438 reservedCapacity
439 ordinary
440 reserved
441 bound)
442 captureExtentMaximum)
443 (arenaCertificate
444 (telemetryPolicyArenaBytes
445 applicationBytes
446 ordinaryCapacity
447 reservedCapacity
448 ordinary
449 reserved
450 bound)
451 (constructor
452 ArenaResidents
453 ArenaResidentsNext
454 (constructor
455 ArenaResident
456 ArenaResidentValue
457 b"capture-policy-decision"
458 (telemetryPolicyDecisionAt
459 applicationBytes
460 ordinaryCapacity
461 reservedCapacity
462 ordinary
463 reserved
464 bound)
465 (naturalMultiply 2 captureWordBytes)
466 captureWordBytes)
467 (telemetryDrainResidents
468 applicationBytes
469 ordinaryCapacity
470 reservedCapacity
471 ordinary
472 reserved
473 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.