84def telemetryDrainDescriptorAdmission =
85 (lambda unrestricted line : Bytes .
86 (naturalAnd
87 (telemetryRecordBytesAdmission line)
88 (eliminate
89 AosLine
90 (lambda unrestricted current : (family AosLine) . Nat)
91 (aosClassifyLine line)
92 (branch AosLineInvalid code . 0)
93 (branch
94 AosLineValid
95 record
96 .
97 (naturalAnd
98 (bytes-equal (aosMemberBytes b"type" record) b"descriptor")
99 (naturalAnd
100 (naturalIsZero (bytes-equal (aosMemberBytes b"kind" record) b"attempt"))
101 (aosChoose
102 Nat
103 (bytes-equal (aosMemberBytes b"kind" record) b"schema")
104 (naturalAnd
105 (naturalNonzero
106 (bytes-length (aosMemberBytes b"schema_id" (aosMemberValue b"body" record))))
107 (aosIsRecordClass
108 (aosMemberBytes b"record_class" (aosMemberValue b"body" record))))
109 1)))))))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.