Source declarations own record recipes. The fixed-recipe plan keeps the
compact existing layout; the routed plan adds one bounded tag per physical
capture slot. Neither infers a schema from payload values or queue position.
A Ready value is validated compiled data, not an unforgeable proof token.
Construct with compile-time (telemetryDrainPlan ...), as for record plans.
21family TelemetryDrainPlan : Type 0
22constructor TelemetryDrainReady
23field unrestricted telemetryDrainOrdinaryCapacity : Nat
24field unrestricted telemetryDrainReservedCapacity : Nat
25field unrestricted telemetryDrainOrdinaryRecord : (family TelemetryRecordPlan)
26field unrestricted telemetryDrainReservedRecord : (family TelemetryRecordPlan)
27field unrestricted telemetryDrainDescriptors : Bytes
28field unrestricted telemetryDrainBodyBound : Nat
29constructor TelemetryDrainRefused
30field unrestricted telemetryDrainRefusal : BytesThe compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.