475def telemetryPolicySiteLookup =
476 (lambda unrestricted wanted : Nat .
477 (lambda unrestricted sites : (family TelemetryPolicySites) .
478 (eliminate
479 TelemetryPolicySites
480 (lambda unrestricted current : (family TelemetryPolicySites) .
481 (family TelemetryPolicySites))
482 sites
483 (branch
484 TelemetryPolicySitesEnd
485 .
486 (constructor TelemetryPolicySites TelemetryPolicySitesEnd))
487 (branch
488 TelemetryPolicySitesNext
489 tag
490 site
491 declaration
492 following
493 induction
494 .
495 (aosChoose
496 (family TelemetryPolicySites)
497 (naturalEqual wanted tag)
498 (constructor
499 TelemetryPolicySites
500 TelemetryPolicySitesNext
501 tag
502 site
503 declaration
504 (constructor TelemetryPolicySites TelemetryPolicySitesEnd))
505 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.