package coq-idxassoc

We define the associative array (key -> value associations) datatype as list of couples, providing definitions of standards operations such as adding, deleting.

We introduce predicates for membership of a key and of couples.

Finally we define a search operator ("find") which returns the value associated with a key or the "none" option (see file Option.v which should be part of this contribution) on failure.

Lemmas we prove about these concepts were motivated by our needs at the moment we created this file. We hope they'll suit your needs too but anyway, feel free to communicate any wish or remark.