310def drainQueueCommands =
311 (lambda unrestricted applicationBytes : Nat .
312 (lambda unrestricted ordinaryCapacity : Nat .
313 (lambda unrestricted reservedCapacity : Nat .
314 (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
315 (lambda unrestricted reserved : (family TelemetryRecordPlan) .
316 (lambda unrestricted bound : Nat .
317 (lambda unrestricted recipe : (family TelemetryRecordPlan) .
318 (lambda unrestricted sourceAt : Nat .
319 (lambda unrestricted occupiedAt : Nat .
320 (lambda unrestricted resultSlot : Nat .
321 (lambda unrestricted identity : Bytes .
322 (lambda unrestricted tail : (family NativePhysicalCommands) .
323 (aosChoose
324 (family NativePhysicalCommands)
325 (naturalNonzero
326 (aosChoose
327 Nat
328 (naturalEqual occupiedAt captureOrdinaryUsedAt)
329 ordinaryCapacity
330 reservedCapacity))
331 (drainOccupiedQueueWith
332 applicationBytes
333 ordinaryCapacity
334 reservedCapacity
335 (drainRecordCommands
336 applicationBytes
337 ordinaryCapacity
338 reservedCapacity
339 bound
340 (telemetryDrainScratchBytesForCapacities
341 ordinaryCapacity
342 reservedCapacity
343 ordinary
344 reserved)
345 recipe
346 resultSlot
347 identity)
348 sourceAt
349 occupiedAt
350 resultSlot
351 identity
352 tail)
353 tail)))))))))))))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.