AlphaGitHub
Source/Packages

Runtime.NativeTelemetryDrain

packages/execution/src/Runtime/NativeTelemetryDrain.alpha

1,049 lines25 declarations49.5 KiBSHA-256 9b04cf809111
Download exact fileView at revision426597bda5753d86c4

def · lines 599–611

drainCommitTagRoutine

Full file
Route metadata is committed immediately after the shared capture primitive. Publication cannot run between those commands. An unexpected tag failure leaves an unroutable capture queued, never a falsely acknowledged event.
599def drainCommitTagRoutine =
600  (lambda unrestricted ordinaryCapacity : Nat .
601    (lambda unrestricted reservedCapacity : Nat .
602      (lambda unrestricted role : Nat .
603        (lambda unrestricted tag : Nat .
604          (nativeTelemetryDrainRoutineFor
605            (constructor
606              TelemetryDrainRoutineKind
607              TelemetryDrainCommitTagRoutine
608              ordinaryCapacity
609              reservedCapacity
610              role
611              tag))))))

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.