the list with the producer of `key` replaced by `update` of what was there
(appended when absent)
198def aosUpsert =
199 (lambda unrestricted key : Bytes .
200 (lambda unrestricted update : (pi unrestricted found : (family AosFound) . (family AosProducer)) .
201 (lambda unrestricted producers : (family StdList (family AosProducer)) .
202 (eliminate
203 StdList
204 (lambda unrestricted current : (family StdList (family AosProducer)) .
205 (family StdList (family AosProducer)))
206 producers
207 (branch
208 StdListEmpty
209 .
210 (constructor
211 StdList
212 StdListCons
213 (family AosProducer)
214 (update (constructor AosFound AosFoundNone))
215 (constructor StdList StdListEmpty (family AosProducer))))
216 (branch
217 StdListCons
218 head
219 tail
220 induction
221 .
222 (aosChoose
223 (family StdList (family AosProducer))
224 (bytes-equal (aosKeyOf head) key)
225 (constructor
226 StdList
227 StdListCons
228 (family AosProducer)
229 (update (constructor AosFound AosFoundSome head))
230 tail)
231 (constructor StdList StdListCons (family AosProducer) head 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.