709def drainDispatchRecordCommands =
710 (lambda unrestricted applicationBytes : Nat .
711 (lambda unrestricted ordinaryCapacity : Nat .
712 (lambda unrestricted reservedCapacity : Nat .
713 (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
714 (lambda unrestricted reserved : (family TelemetryRecordPlan) .
715 (lambda unrestricted bound : Nat .
716 (lambda unrestricted routes : (family TelemetryRecordRoutes) .
717 (lambda unrestricted resultSlot : Nat .
718 (lambda unrestricted identity : Bytes .
719 (lambda unrestricted tail : (family NativePhysicalCommands) .
720 (nativeLaunchRecipeCommand
721 (constructor
722 NativePhysicalOperation
723 NativePhysicalMachineRoutine
724 (drainReadTagRoutine ordinaryCapacity reservedCapacity routes)
725 (constructor
726 NativePhysicalArguments
727 NativePhysicalArgumentsValue
728 (publicationStateAddress
729 applicationBytes
730 ordinaryCapacity
731 reservedCapacity
732 0)
733 (publicationStateLoad
734 applicationBytes
735 ordinaryCapacity
736 reservedCapacity
737 publicationSavedR13At)
738 (drainState (captureQueueAt applicationBytes))
739 (drainState
740 (telemetryDispatchTagsAt
741 applicationBytes
742 ordinaryCapacity
743 reservedCapacity
744 ordinary
745 reserved
746 bound))
747 (nativeLaunchRecipeImmediate
748 (telemetryDispatchTagsBytes ordinaryCapacity reservedCapacity))
749 (drainState
750 (telemetryDispatchTagScratchAt
751 applicationBytes
752 ordinaryCapacity
753 reservedCapacity
754 ordinary
755 reserved
756 bound)))
757 (nativeLaunchRecipeStore resultSlot))
758 identity
759 (nativeLaunchRecipeCommand
760 (constructor
761 NativePhysicalOperation
762 NativePhysicalRepeatBeginCounted
763 (nativeLaunchRecipeSlotValue resultSlot))
764 identity
765 (drainRenderRoutes
766 applicationBytes
767 ordinaryCapacity
768 reservedCapacity
769 ordinary
770 reserved
771 bound
772 routes
773 resultSlot
774 identity
775 (nativeLaunchRecipeCommand
776 (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
777 identity
778 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.