346def telemetryDrainArenaBytes =
347 (lambda unrestricted applicationBytes : Nat .
348 (lambda unrestricted ordinaryCapacity : Nat .
349 (lambda unrestricted reservedCapacity : Nat .
350 (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
351 (lambda unrestricted reserved : (family TelemetryRecordPlan) .
352 (lambda unrestricted bound : Nat .
353 (naturalAdd
354 (telemetryDrainScratchAt applicationBytes ordinaryCapacity reservedCapacity bound)
355 (telemetryDrainScratchBytesForCapacities
356 ordinaryCapacity
357 reservedCapacity
358 ordinary
359 reserved))))))))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.