735def telemetryRoutedPolicyArenaBytes =
736 (lambda unrestricted applicationBytes : Nat .
737 (lambda unrestricted ordinaryCapacity : Nat .
738 (lambda unrestricted reservedCapacity : Nat .
739 (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
740 (lambda unrestricted reserved : (family TelemetryRecordPlan) .
741 (lambda unrestricted bound : Nat .
742 (naturalAdd
743 (telemetryRoutedPolicyDecisionAt
744 applicationBytes
745 ordinaryCapacity
746 reservedCapacity
747 ordinary
748 reserved
749 bound)
750 (naturalMultiply 2 captureWordBytes))))))))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.