176def aosFind =
177 (lambda unrestricted key : Bytes .
178 (lambda unrestricted producers : (family StdList (family AosProducer)) .
179 (eliminate
180 StdList
181 (lambda unrestricted current : (family StdList (family AosProducer)) . (family AosFound))
182 producers
183 (branch StdListEmpty . (constructor AosFound AosFoundNone))
184 (branch
185 StdListCons
186 head
187 tail
188 induction
189 .
190 (aosChoose
191 (family AosFound)
192 (bytes-equal (aosKeyOf head) key)
193 (constructor AosFound AosFoundSome head)
194 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.