Multiset of keys of an association multiset.

nodupkeys s means that s has no duplicate keys.

finmap β is the type of finite maps over a multiset. It is effectively a quotient of alist β by permutation of the underlying list.

The quotient map from alist to finmap.

Lift a permutation-respecting function on alist to finmap.

Lift a permutation-respecting function on 2 alists to 2 finmaps.

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

The set of keys of a finite map.

The empty map.

The singleton map.

Look up the value associated to a key in a map.

Replace a key with a given value in a finite map. If the key is not present it does nothing.

Fold a commutative 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 a finite map, replacing 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 finite maps. It is left-biased: if there exists an a ∈ s₁, lookup a (s₁ ∪ s₂) = lookup a s₁.