312def telemetryDrainScratchBytesForCapacities =
313 (lambda unrestricted ordinaryCapacity : Nat .
314 (lambda unrestricted reservedCapacity : Nat .
315 (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
316 (lambda unrestricted reserved : (family TelemetryRecordPlan) .
317 (naturalAdd
318 telemetryRecordAt
319 (telemetryDrainMaximum
320 (aosChoose
321 Nat
322 (naturalNonzero ordinaryCapacity)
323 (telemetryDrainRecordBytes ordinary)
324 0)
325 (aosChoose
326 Nat
327 (naturalNonzero reservedCapacity)
328 (telemetryDrainRecordBytes reserved)
329 0)))))))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.