164def telemetryDrainDescriptorsAdmission =
165 (lambda unrestricted descriptors : (family StdList Bytes) .
166 (eliminate
167 StdList
168 (lambda unrestricted current : (family StdList Bytes) . Nat)
169 descriptors
170 (branch StdListEmpty . 1)
171 (branch
172 StdListCons
173 head
174 tail
175 induction
176 .
177 (naturalAnd
178 induction
179 (naturalAnd
180 (telemetryDrainDescriptorAdmission head)
181 (telemetryDrainDistinctDescriptor head tail))))))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.