630def drainRenderRoutes =
631 (lambda unrestricted applicationBytes : Nat .
632 (lambda unrestricted ordinaryCapacity : Nat .
633 (lambda unrestricted reservedCapacity : Nat .
634 (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
635 (lambda unrestricted reserved : (family TelemetryRecordPlan) .
636 (lambda unrestricted bound : Nat .
637 (lambda unrestricted routes : (family TelemetryRecordRoutes) .
638 (lambda unrestricted resultSlot : Nat .
639 (lambda unrestricted identity : Bytes .
640 (lambda unrestricted tail : (family NativePhysicalCommands) .
641 (app
642 (eliminate
643 TelemetryRecordRoutes
644 (lambda unrestricted current : (family TelemetryRecordRoutes) .
645 (pi unrestricted commands : (family NativePhysicalCommands) .
646 (family NativePhysicalCommands)))
647 routes
648 (branch
649 TelemetryRecordRoutesEnd
650 .
651 (lambda unrestricted commands : (family NativePhysicalCommands) .
652 commands))
653 (branch
654 TelemetryRecordRoutesNext
655 tag
656 recipe
657 following
658 induction
659 .
660 (lambda unrestricted commands : (family NativePhysicalCommands) .
661 (nativeLaunchRecipeCommand
662 (constructor
663 NativePhysicalOperation
664 NativePhysicalMachineRoutine
665 (drainMatchTagRoutine tag)
666 (constructor
667 NativePhysicalArguments
668 NativePhysicalArgumentsValue
669 (drainState
670 (telemetryDispatchTagScratchAt
671 applicationBytes
672 ordinaryCapacity
673 reservedCapacity
674 ordinary
675 reserved
676 bound))
677 (nativeLaunchRecipeImmediate 0)
678 (nativeLaunchRecipeImmediate 0)
679 (nativeLaunchRecipeImmediate 0)
680 (nativeLaunchRecipeImmediate 0)
681 (nativeLaunchRecipeImmediate 0))
682 (nativeLaunchRecipeStore resultSlot))
683 identity
684 (nativeLaunchRecipeCommand
685 (constructor
686 NativePhysicalOperation
687 NativePhysicalRepeatBeginCounted
688 (nativeLaunchRecipeSlotValue resultSlot))
689 identity
690 (drainRecordCommands
691 applicationBytes
692 ordinaryCapacity
693 reservedCapacity
694 bound
695 (telemetryDrainScratchBytesForCapacities
696 ordinaryCapacity
697 reservedCapacity
698 ordinary
699 reserved)
700 recipe
701 resultSlot
702 identity
703 (nativeLaunchRecipeCommand
704 (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
705 identity
706 (induction commands))))))))
707 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.