401def telemetryPolicyArenaBytes =
402 (lambda unrestricted applicationBytes : Nat .
403 (lambda unrestricted ordinaryCapacity : Nat .
404 (lambda unrestricted reservedCapacity : Nat .
405 (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
406 (lambda unrestricted reserved : (family TelemetryRecordPlan) .
407 (lambda unrestricted bound : Nat .
408 (naturalAdd
409 (telemetryPolicyDecisionAt
410 applicationBytes
411 ordinaryCapacity
412 reservedCapacity
413 ordinary
414 reserved
415 bound)
416 (naturalMultiply 2 captureWordBytes))))))))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.