112def nativeTelemetrySourcesAdmission =
113 (lambda unrestricted recipe : (family TelemetryRecordPlan) .
114 (lambda unrestricted values : (family NativeTelemetrySourceValues) .
115 (eliminate
116 TelemetryRecordPlan
117 (lambda unrestricted current : (family TelemetryRecordPlan) . Nat)
118 recipe
119 (branch
120 TelemetryRecordReady
121 parts
122 template
123 .
124 (nat-eliminate
125 (lambda unrestricted count : Nat . Nat)
126 1
127 (lambda unrestricted index : Nat .
128 (lambda unrestricted induction : Nat .
129 (naturalAnd
130 induction
131 (naturalOr
132 (naturalIsZero (telemetryRecordWordRequired parts index))
133 (nativeTelemetrySourcePresent (nativeTelemetrySourceAt values index))))))
134 captureValueWords))
135 (branch TelemetryRecordRefused reason . 0))))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.