247def telemetryDrainPlanAtContexts =
248 (lambda unrestricted ordinaryContext : Bytes .
249 (lambda unrestricted reservedContext : Bytes .
250 (lambda unrestricted ordinaryCapacity : Nat .
251 (lambda unrestricted reservedCapacity : Nat .
252 (lambda unrestricted ordinary : (family TelemetryRecordDeclaration) .
253 (lambda unrestricted reserved : (family TelemetryRecordDeclaration) .
254 (lambda unrestricted descriptors : (family StdList Bytes) .
255 (let unrestricted ordinaryPlan =
256 (telemetryRecordPlanAtContext ordinaryContext ordinary)
257 in
258 (let unrestricted reservedPlan =
259 (telemetryRecordPlanAtContext reservedContext reserved)
260 in
261 (let unrestricted descriptorBytes =
262 (publicationTypedRecordBytes descriptors)
263 in
264 (let unrestricted bound =
265 (telemetryDrainBound
266 ordinaryCapacity
267 reservedCapacity
268 ordinaryPlan
269 reservedPlan
270 descriptorBytes)
271 in
272 (aosChoose
273 (family TelemetryDrainPlan)
274 (naturalAnd
275 (naturalLessOrEqual 2 reservedCapacity)
276 (naturalAnd
277 (naturalLessOrEqual
278 (naturalAdd
279 (naturalAdd ordinaryCapacity reservedCapacity)
280 (aosListLength descriptors))
281 1024)
282 (naturalAnd
283 (naturalNonzero (telemetryDrainRecordBytes ordinaryPlan))
284 (naturalAnd
285 (naturalNonzero (telemetryDrainRecordBytes reservedPlan))
286 (naturalAnd
287 (telemetryDrainDescriptorsAdmission descriptors)
288 (naturalAnd
289 (telemetryDrainSchemaAdmission ordinary descriptors)
290 (naturalAnd
291 (telemetryDrainSchemaAdmission reserved descriptors)
292 (naturalLessOrEqual
293 (publicationRecordBytes bound)
294 publicationMaximumFrameBytes))))))))
295 (constructor
296 TelemetryDrainPlan
297 TelemetryDrainReady
298 ordinaryCapacity
299 reservedCapacity
300 ordinaryPlan
301 reservedPlan
302 descriptorBytes
303 bound)
304 (constructor
305 TelemetryDrainPlan
306 TelemetryDrainRefused
307 b"native-typed-drain-declaration-refused")))))))))))))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.