769def telemetryDispatchResidents =
770 (lambda unrestricted applicationBytes : Nat .
771 (lambda unrestricted ordinaryCapacity : Nat .
772 (lambda unrestricted reservedCapacity : Nat .
773 (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
774 (lambda unrestricted reserved : (family TelemetryRecordPlan) .
775 (lambda unrestricted bound : Nat .
776 (constructor
777 ArenaResidents
778 ArenaResidentsNext
779 (constructor
780 ArenaResident
781 ArenaResidentValue
782 b"typed-drain-route-tags"
783 (telemetryDispatchTagsAt
784 applicationBytes
785 ordinaryCapacity
786 reservedCapacity
787 ordinary
788 reserved
789 bound)
790 (naturalAdd
791 captureWordBytes
792 (telemetryDispatchTagsBytes ordinaryCapacity reservedCapacity))
793 captureWordBytes)
794 (telemetryDrainResidents
795 applicationBytes
796 ordinaryCapacity
797 reservedCapacity
798 ordinary
799 reserved
800 bound))))))))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.