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 714–728

telemetryDispatchTagsAt

Full file
Route tags and one private dispatch word follow the existing derived arena. Capture values, identities and the version-two wire shape remain unchanged.
714def telemetryDispatchTagsAt =
715  (lambda unrestricted applicationBytes : Nat .
716    (lambda unrestricted ordinaryCapacity : Nat .
717      (lambda unrestricted reservedCapacity : Nat .
718        (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
719          (lambda unrestricted reserved : (family TelemetryRecordPlan) .
720            (lambda unrestricted bound : Nat .
721              (captureAlign
722                (telemetryDrainArenaBytes
723                  applicationBytes
724                  ordinaryCapacity
725                  reservedCapacity
726                  ordinary
727                  reserved
728                  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.