bucket_array α β is the underlying data type for hash_map α β, an array of linked lists of key-value pairs.

Make a hash_map index from a nat hash value and a (positive) buffer size

Read the bucket corresponding to an element

Write the bucket corresponding to an element

Modify (read, apply f, and write) the bucket corresponding to an element

The list of all key-value pairs in the bucket list

Fold a function f over the key-value pairs in the bucket list

Insert the pair ⟨a, b⟩ into the correct location in the bucket array (without checking for duplication)

Search a bucket for a key a and return the value

Returns tt if the bucket l contains the key a

Modify a bucket to replace a value in the list. Leaves the list unchanged if the key is not found.

Modify a bucket to remove a key, if it exists.

The predicate valid bkts sz means that bkts satisfies the hash_map invariants: There are exactly sz elements in it, every pair is in the bucket determined by its key and the hash function, and no key appears multiple times in the list.

A hash map data structure, representing a finite key-value map with key type α and value type β (which may depend on α).

Construct an empty hash map with buffer size nbuckets (default 8).

Return the value corresponding to a key, or none if not found

Return tt if the key exists in the map

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

The list of key-value pairs in the map

The list of keys in the map

Insert a key-value pair into the map. (Modifies m in-place when applicable)

Insert a list of key-value pairs into the map. (Modifies m in-place when applicable)

Construct a hash map from a list of key-value pairs.

Remove a key from the map. (Modifies m in-place when applicable)