alist β is a key-value map stored as a list (i.e. a linked list). It is a wrapper around certain list functions with the added constraint that the list have unique keys.

The list of keys of an association list.

The predicate a ∈ s means that s has a value associated to the key a.

The empty association list.

The singleton association list.

Look up the value associated to a key in an association list.

Replace a key with a given value in an association list. If the key is not present it does nothing.

Fold a function over the key-value pairs in the map.

Erase a key from the map. If the key is not present it does nothing.

Insert a key-value pair into an association list and erase any existing pair with the same key.

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₁.