752def telemetryRoutedPolicyArenaCertificate =
753 (lambda unrestricted applicationBytes : Nat .
754 (lambda unrestricted ordinaryCapacity : Nat .
755 (lambda unrestricted reservedCapacity : Nat .
756 (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
757 (lambda unrestricted reserved : (family TelemetryRecordPlan) .
758 (lambda unrestricted bound : Nat .
759 (naturalAnd
760 (telemetryDispatchArenaCertificate
761 applicationBytes
762 ordinaryCapacity
763 reservedCapacity
764 ordinary
765 reserved
766 bound)
767 (naturalAnd
768 (naturalLessOrEqual
769 (telemetryRoutedPolicyArenaBytes
770 applicationBytes
771 ordinaryCapacity
772 reservedCapacity
773 ordinary
774 reserved
775 bound)
776 captureExtentMaximum)
777 (arenaCertificate
778 (telemetryRoutedPolicyArenaBytes
779 applicationBytes
780 ordinaryCapacity
781 reservedCapacity
782 ordinary
783 reserved
784 bound)
785 (constructor
786 ArenaResidents
787 ArenaResidentsNext
788 (constructor
789 ArenaResident
790 ArenaResidentValue
791 b"routed-policy-decision"
792 (telemetryRoutedPolicyDecisionAt
793 applicationBytes
794 ordinaryCapacity
795 reservedCapacity
796 ordinary
797 reserved
798 bound)
799 (naturalMultiply 2 captureWordBytes)
800 captureWordBytes)
801 (telemetryDispatchResidents
802 applicationBytes
803 ordinaryCapacity
804 reservedCapacity
805 ordinary
806 reserved
807 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.