AlphaGitHub
Source/Packages

Runtime.TelemetryDrain

packages/execution/src/Runtime/TelemetryDrain.alpha

867 lines66 declarations34.3 KiBSHA-256 7229c44d3f7b
Download exact fileView at revision426597bda5753d86c4

def · lines 231–245

telemetryDrainBound

Full file
231def telemetryDrainBound =
232  (lambda unrestricted ordinaryCapacity : Nat .
233    (lambda unrestricted reservedCapacity : Nat .
234      (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
235        (lambda unrestricted reserved : (family TelemetryRecordPlan) .
236          (lambda unrestricted descriptors : Bytes .
237            (telemetryDrainMaximum
238              (publicationBodyMaximumBytes ordinaryCapacity reservedCapacity)
239              (naturalAdd
240                publicationPayloadRecordsAt
241                (naturalAdd
242                  (bytes-length descriptors)
243                  (naturalAdd
244                    (naturalMultiply ordinaryCapacity (succ (telemetryDrainRecordBytes ordinary)))
245                    (naturalMultiply reservedCapacity (succ (telemetryDrainRecordBytes reserved))))))))))))

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.