486def telemetryRouteContextAdmission =
487 (lambda unrestricted context : Bytes .
488 (lambda unrestricted descriptors : (family StdList Bytes) .
489 (aosChoose
490 Nat
491 (bytes-equal context b"")
492 1
493 (eliminate
494 StdList
495 (lambda unrestricted current : (family StdList Bytes) . Nat)
496 descriptors
497 (branch StdListEmpty . 0)
498 (branch
499 StdListCons
500 head
501 tail
502 induction
503 .
504 (naturalOr
505 induction
506 (eliminate
507 AosLine
508 (lambda unrestricted current : (family AosLine) . Nat)
509 (aosClassifyLine head)
510 (branch AosLineInvalid code . 0)
511 (branch
512 AosLineValid
513 record
514 .
515 (naturalAnd
516 (bytes-equal (aosMemberBytes b"kind" record) b"context")
517 (bytes-equal
518 context
519 (aosMemberBytes b"context_id" (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.