534def telemetryPolicySelectedRoutes =
535 (lambda unrestricted policy : (family CapturePolicy) .
536 (lambda unrestricted role : Nat .
537 (lambda unrestricted sites : (family TelemetryPolicySites) .
538 (eliminate
539 TelemetryPolicySites
540 (lambda unrestricted current : (family TelemetryPolicySites) .
541 (family TelemetryRouteDeclarations))
542 sites
543 (branch
544 TelemetryPolicySitesEnd
545 .
546 (constructor TelemetryRouteDeclarations TelemetryRouteDeclarationsEnd))
547 (branch
548 TelemetryPolicySitesNext
549 tag
550 site
551 declaration
552 following
553 induction
554 .
555 (aosChoose
556 (family TelemetryRouteDeclarations)
557 (naturalAnd
558 (captureSiteSelected policy site)
559 (naturalEqual role (captureSiteReserved site)))
560 (constructor
561 TelemetryRouteDeclarations
562 TelemetryRouteDeclarationsNext
563 tag
564 (captureSiteIdentifier site)
565 declaration
566 induction)
567 induction))))))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.