Association Lists #
This file defines association lists. An association list is a list where every element consists of a key and a value, and no two entries have the same key. The type of the value is allowed to be dependent on the type of the key.
Main definitions #
alist.keysreturns a list of keys of the alist.
alist.memreturns membership in the set of keys.
alist.eraseremoves a certain key.
alist.insertadds a key-value mapping to the list.
alist.unioncombines two association lists.
Erase a key from the map, and return the corresponding value, if found.
s₁ ∪ s₂ is the key-based union of two association lists. It is
left-biased: if there exists an
a ∈ s₁,
lookup a (s₁ ∪ s₂) = lookup a s₁.