780def drainDispatchQueueCommands =
781 (lambda unrestricted applicationBytes : Nat .
782 (lambda unrestricted ordinaryCapacity : Nat .
783 (lambda unrestricted reservedCapacity : Nat .
784 (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
785 (lambda unrestricted reserved : (family TelemetryRecordPlan) .
786 (lambda unrestricted bound : Nat .
787 (lambda unrestricted routes : (family TelemetryRecordRoutes) .
788 (lambda unrestricted sourceAt : Nat .
789 (lambda unrestricted occupiedAt : Nat .
790 (lambda unrestricted resultSlot : Nat .
791 (lambda unrestricted identity : Bytes .
792 (lambda unrestricted tail : (family NativePhysicalCommands) .
793 (aosChoose
794 (family NativePhysicalCommands)
795 (naturalNonzero
796 (aosChoose
797 Nat
798 (naturalEqual occupiedAt captureOrdinaryUsedAt)
799 ordinaryCapacity
800 reservedCapacity))
801 (drainOccupiedQueueWith
802 applicationBytes
803 ordinaryCapacity
804 reservedCapacity
805 (drainDispatchRecordCommands
806 applicationBytes
807 ordinaryCapacity
808 reservedCapacity
809 ordinary
810 reserved
811 bound
812 routes
813 resultSlot
814 identity)
815 sourceAt
816 occupiedAt
817 resultSlot
818 identity
819 tail)
820 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.