752def telemetryDispatchArenaBytes =
753 (lambda unrestricted applicationBytes : Nat .
754 (lambda unrestricted ordinaryCapacity : Nat .
755 (lambda unrestricted reservedCapacity : Nat .
756 (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
757 (lambda unrestricted reserved : (family TelemetryRecordPlan) .
758 (lambda unrestricted bound : Nat .
759 (naturalAdd
760 captureWordBytes
761 (telemetryDispatchTagScratchAt
762 applicationBytes
763 ordinaryCapacity
764 reservedCapacity
765 ordinary
766 reserved
767 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.