183def telemetryDrainSchemaAdmission =
184 (lambda unrestricted declaration : (family TelemetryRecordDeclaration) .
185 (lambda unrestricted descriptors : (family StdList Bytes) .
186 (eliminate
187 TelemetryRecordDeclaration
188 (lambda unrestricted current : (family TelemetryRecordDeclaration) . Nat)
189 declaration
190 (branch
191 TelemetryRecordDeclarationValue
192 schema
193 recordClass
194 policy
195 origin
196 method
197 payload
198 .
199 (eliminate
200 StdList
201 (lambda unrestricted current : (family StdList Bytes) . Nat)
202 descriptors
203 (branch StdListEmpty . 0)
204 (branch
205 StdListCons
206 head
207 tail
208 induction
209 .
210 (naturalOr
211 induction
212 (eliminate
213 AosLine
214 (lambda unrestricted current : (family AosLine) . Nat)
215 (aosClassifyLine head)
216 (branch AosLineInvalid code . 0)
217 (branch
218 AosLineValid
219 record
220 .
221 (naturalAnd
222 (bytes-equal (aosMemberBytes b"kind" record) b"schema")
223 (naturalAnd
224 (bytes-equal
225 schema
226 (aosMemberBytes b"schema_id" (aosMemberValue b"body" record)))
227 (bytes-equal
228 recordClass
229 (aosMemberBytes b"record_class" (aosMemberValue b"body" record))))))))))))))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.