361def telemetryDrainResidents =
362 (lambda unrestricted applicationBytes : Nat .
363 (lambda unrestricted ordinaryCapacity : Nat .
364 (lambda unrestricted reservedCapacity : Nat .
365 (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
366 (lambda unrestricted reserved : (family TelemetryRecordPlan) .
367 (lambda unrestricted bound : Nat .
368 (constructor
369 ArenaResidents
370 ArenaResidentsNext
371 (constructor
372 ArenaResident
373 ArenaResidentValue
374 b"typed-drain-record"
375 (telemetryDrainScratchAt applicationBytes ordinaryCapacity reservedCapacity bound)
376 (telemetryDrainScratchBytesForCapacities
377 ordinaryCapacity
378 reservedCapacity
379 ordinary
380 reserved)
381 captureWordBytes)
382 (publicationWholeArenaResidentsForBody
383 applicationBytes
384 ordinaryCapacity
385 reservedCapacity
386 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.