569def telemetryPolicySitesAdmission =
570 (lambda unrestricted policy : (family CapturePolicy) .
571 (lambda unrestricted sites : (family TelemetryPolicySites) .
572 (eliminate
573 TelemetryPolicySites
574 (lambda unrestricted current : (family TelemetryPolicySites) . Nat)
575 sites
576 (branch TelemetryPolicySitesEnd . 1)
577 (branch
578 TelemetryPolicySitesNext
579 tag
580 site
581 declaration
582 following
583 induction
584 .
585 (naturalAnd
586 induction
587 (naturalAnd
588 (captureSiteAdmission policy site)
589 (telemetryPolicyRecordAdmission policy 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.