521def telemetryRouteDeclarationsAdmission =
522 (lambda unrestricted declarations : (family TelemetryRouteDeclarations) .
523 (lambda unrestricted other : (family TelemetryRouteDeclarations) .
524 (lambda unrestricted descriptors : (family StdList Bytes) .
525 (eliminate
526 TelemetryRouteDeclarations
527 (lambda unrestricted current : (family TelemetryRouteDeclarations) . Nat)
528 declarations
529 (branch TelemetryRouteDeclarationsEnd . 1)
530 (branch
531 TelemetryRouteDeclarationsNext
532 tag
533 context
534 declaration
535 tail
536 induction
537 .
538 (naturalAnd
539 induction
540 (naturalAnd
541 (naturalNonzero tag)
542 (naturalAnd
543 (naturalLessOrEqual tag 1024)
544 (naturalAnd
545 (naturalIsZero (telemetryRouteDeclaredContains tag tail))
546 (naturalAnd
547 (naturalIsZero (telemetryRouteDeclaredContains tag other))
548 (naturalAnd
549 (telemetryRouteContextAdmission context descriptors)
550 (naturalAnd
551 (telemetryDrainSchemaAdmission declaration descriptors)
552 (naturalNonzero
553 (telemetryDrainRecordBytes
554 (telemetryRecordPlanAtContext context declaration)))))))))))))))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.