@[reducible, inline]

abbrev Data.IntMap (v : Type u) : Type u

A map from Nat keys to values, backed by a hash map. $$\text{IntMap}(v) \cong \text{HashMap}(\mathbb{N}, v)$$ Provides amortised $O(1)$ lookup and insert.

Equations

• Data.IntMap v = Std.HashMap Nat v

@[inline]

def Data.IntMap.empty {v : Type u} : IntMap v

The empty map. $$\text{empty} = \emptyset$$

Equations

• Data.IntMap.empty = ∅

@[inline]

def Data.IntMap.singleton {v : Type u} (key : Nat) (val : v) : IntMap v

A map with a single key-value pair. $$\text{singleton}(k, v) = \{k \mapsto v\}$$

Equations

• Data.IntMap.singleton key val = Std.HashMap.insert ∅ key val

@[inline]

def Data.IntMap.fromList {v : Type u} (l : List (Nat × v)) : IntMap v

Build a map from an association list. Later entries override earlier ones for duplicate keys. $$\text{fromList}([(k_1,v_1),\ldots,(k_n,v_n)])$$

Equations

• Data.IntMap.fromList l = Std.HashMap.ofList l

@[inline]

def Data.IntMap.lookup {v : Type u} (key : Nat) (m : IntMap v) : Option v

Look up a key. $$\text{lookup}(k, m) = \begin{cases} \text{some}(v) & \text{if } k \mapsto v \in m \\ \text{none} & \text{otherwise} \end{cases}$$

Equations

• Data.IntMap.lookup key m = Std.HashMap.get? m key

@[inline]

def Data.IntMap.findWithDefault {v : Type u} (dflt : v) (key : Nat) (m : IntMap v) : v

Look up a key, returning a default if absent. $$\text{findWithDefault}(d, k, m) = \begin{cases} v & \text{if } k \mapsto v \in m \\ d & \text{otherwise} \end{cases}$$

Equations

• Data.IntMap.findWithDefault dflt key m = (Std.HashMap.get? m key).getD dflt

@[inline]

def Data.IntMap.member {v : Type u} (key : Nat) (m : IntMap v) : Bool

Test whether a key is in the map. $$\text{member}(k, m) \iff k \in \text{dom}(m)$$

Equations

• Data.IntMap.member key m = Std.HashMap.contains m key

@[inline]

def Data.IntMap.null {v : Type u} (m : IntMap v) : Bool

Is the map empty? $$\text{null}(m) \iff m = \emptyset$$

Equations

• m.null = Std.HashMap.isEmpty m

@[inline]

def Data.IntMap.size' {v : Type u} (m : IntMap v) : Nat

The number of entries. $$\text{size'}(m) = |m|$$

Equations

• m.size' = Std.HashMap.size m

@[inline]

def Data.IntMap.insert' {v : Type u} (key : Nat) (val : v) (m : IntMap v) : IntMap v

Insert a key-value pair. If the key already exists, the value is replaced. $$\text{insert}(k, v, m) = m[k \mapsto v]$$

Equations

• Data.IntMap.insert' key val m = Std.HashMap.insert m key val

@[inline]

def Data.IntMap.delete {v : Type u} (key : Nat) (m : IntMap v) : IntMap v

Delete a key from the map. $$\text{delete}(k, m) = m \setminus \{k\}$$

Equations

• Data.IntMap.delete key m = Std.HashMap.erase m key

def Data.IntMap.adjust {v : Type u} (f : v → v) (key : Nat) (m : IntMap v) : IntMap v

Adjust the value at a key, if present. $$\text{adjust}(f, k, m) = \begin{cases} m[k \mapsto f(v)] & \text{if } k \mapsto v \in m \\ m & \text{otherwise} \end{cases}$$

Equations

• Data.IntMap.adjust f key m = match Std.HashMap.get? m key with | some val => Std.HashMap.insert m key (f val) | none => m

def Data.IntMap.union {v : Type u} (m1 m2 : IntMap v) : IntMap v

Left-biased union of two maps. $$\text{union}(m_1, m_2) = m_1 \cup m_2 \quad (\text{left-biased})$$

Equations

• m1.union m2 = Std.HashMap.fold (fun (acc : Data.IntMap v) (key : Nat) (val : v) => if Std.HashMap.contains acc key = true then acc else Std.HashMap.insert acc key val) m1 m2

def Data.IntMap.unionWith {v : Type u} (f : v → v → v) (m1 m2 : IntMap v) : IntMap v

Union with a combining function. $$\text{unionWith}(f, m_1, m_2)[k] = \begin{cases} f(v_1, v_2) & \text{if } k \in m_1 \cap m_2 \\ v_1 & \text{if } k \in m_1 \text{ only} \\ v_2 & \text{if } k \in m_2 \text{ only} \end{cases}$$

Equations

• One or more equations did not get rendered due to their size.

def Data.IntMap.intersection {v : Type u} (m1 m2 : IntMap v) : IntMap v

Intersection of two maps, keeping values from the first. $$\text{intersection}(m_1, m_2) = \{k \mapsto v \mid k \mapsto v \in m_1, k \in \text{dom}(m_2)\}$$

Equations

• m1.intersection m2 = Std.HashMap.filter (fun (key : Nat) (x : v) => Std.HashMap.contains m2 key) m1

def Data.IntMap.intersectionWith {v : Type u} (f : v → v → v) (m1 m2 : IntMap v) : IntMap v

Intersection with a combining function. $$\text{intersectionWith}(f, m_1, m_2)[k] = f(v_1, v_2) \text{ for } k \in \text{dom}(m_1) \cap \text{dom}(m_2)$$

Equations

• One or more equations did not get rendered due to their size.

def Data.IntMap.difference {v : Type u} (m1 m2 : IntMap v) : IntMap v

Difference of two maps. $$\text{difference}(m_1, m_2) = \{k \mapsto v \mid k \mapsto v \in m_1, k \notin \text{dom}(m_2)\}$$

Equations

• m1.difference m2 = Std.HashMap.filter (fun (key : Nat) (x : v) => !Std.HashMap.contains m2 key) m1

@[inline]

def Data.IntMap.foldlWithKey {v : Type u} {α : Type u_1} (f : α → Nat → v → α) (init : α) (m : IntMap v) : α

Left fold over key-value pairs (unspecified order). $$\text{foldlWithKey}(f, z, m)$$

Equations

• Data.IntMap.foldlWithKey f init m = Std.HashMap.fold (fun (acc : α) (key : Nat) (val : v) => f acc key val) init m

def Data.IntMap.foldrWithKey {v : Type u} {α : Type u_1} (f : Nat → v → α → α) (init : α) (m : IntMap v) : α

Right fold over key-value pairs (unspecified order). $$\text{foldrWithKey}(f, z, m)$$

Equations

• Data.IntMap.foldrWithKey f init m = List.foldr (fun (x : Nat × v) (acc : α) => match x with | (key, val) => f key val acc) init (Std.HashMap.toList m)

@[inline]

def Data.IntMap.mapValues {v : Type u} {w : Type u_1} (f : v → w) (m : IntMap v) : IntMap w

Map a function over all values. $$\text{mapValues}(f, m)[k] = f(m[k])$$

Equations

• Data.IntMap.mapValues f m = Std.HashMap.map (fun (x : Nat) (val : v) => f val) m

@[inline]

def Data.IntMap.mapWithKey {v : Type u} {w : Type u_1} (f : Nat → v → w) (m : IntMap v) : IntMap w

Map a function over all key-value pairs. $$\text{mapWithKey}(f, m)[k] = f(k, m[k])$$

Equations

• Data.IntMap.mapWithKey f m = Std.HashMap.map (fun (key : Nat) (val : v) => f key val) m

@[inline]

def Data.IntMap.filterWithKey {v : Type u} (p : Nat → v → Bool) (m : IntMap v) : IntMap v

Filter entries by a predicate on keys and values. $$\text{filterWithKey}(p, m) = \{k \mapsto v \mid k \mapsto v \in m, p(k, v)\}$$

Equations

• Data.IntMap.filterWithKey p m = Std.HashMap.filter p m

@[inline]

def Data.IntMap.toList' {v : Type u} (m : IntMap v) : List (Nat × v)

Convert the map to a list of key-value pairs (unspecified order). $$\text{toList'}(m) = [(k_1, v_1), \ldots, (k_n, v_n)]$$

Equations

• m.toList' = Std.HashMap.toList m

def Data.IntMap.toAscList {v : Type u} (m : IntMap v) : List (Nat × v)

Convert the map to an association list sorted by ascending key. $$\text{toAscList}(m) = [(k_1, v_1), \ldots, (k_n, v_n)]$$ where $k_1 < \cdots < k_n$. Note: requires $O(n \log n)$ sort since the backing HashMap is unordered.

Equations

• m.toAscList = ((Std.HashMap.toList m).toArray.qsort fun (a b : Nat × v) => decide (a.fst < b.fst)).toList

def Data.IntMap.keys {v : Type u} (m : IntMap v) : List Nat

The list of all keys (unspecified order). $$\text{keys}(m) = [k_1, \ldots, k_n]$$

Equations

• m.keys = Std.HashMap.fold (fun (acc : List Nat) (key : Nat) (x : v) => key :: acc) [] m

def Data.IntMap.elems {v : Type u} (m : IntMap v) : List v

The list of all values (unspecified order). $$\text{elems}(m) = [v_1, \ldots, v_n]$$

Equations

• m.elems = Std.HashMap.fold (fun (acc : List v) (x : Nat) (val : v) => val :: acc) [] m

def Data.IntMap.restrictKeys {v : Type u} (m : IntMap v) (ks : List Nat) : IntMap v

Restrict a map to only the keys in the given list. $$\text{restrictKeys}(m, ks) = \{k \mapsto v \mid k \mapsto v \in m, k \in ks\}$$

Equations

• m.restrictKeys ks = Std.HashMap.filter (fun (key : Nat) (x : v) => (List.foldl (fun (s : Std.HashMap Nat Unit) (key : Nat) => s.insert key ()) ∅ ks).contains key) m

def Data.IntMap.withoutKeys {v : Type u} (m : IntMap v) (ks : List Nat) : IntMap v

Remove all keys in the given list from the map. $$\text{withoutKeys}(m, ks) = \{k \mapsto v \mid k \mapsto v \in m, k \notin ks\}$$

Equations

• m.withoutKeys ks = Std.HashMap.filter (fun (key : Nat) (x : v) => !(List.foldl (fun (s : Std.HashMap Nat Unit) (key : Nat) => s.insert key ()) ∅ ks).contains key) m

def Data.IntMap.isSubmapOf {v : Type u} [BEq v] (m1 m2 : IntMap v) : Bool

Is m1 a submap of m2? $$\text{isSubmapOf}(m_1, m_2) \iff \forall k \in \text{dom}(m_1),\; m_1[k] = m_2[k]$$

Equations

• One or more equations did not get rendered due to their size.

def Data.IntMap.lookupMin {v : Type u} (m : IntMap v) : Option (Nat × v)

The smallest key-value pair, or none if the map is empty. $$\text{lookupMin}(m) = \min_{k} \{(k, v) \mid k \mapsto v \in m\}$$ Note: $O(n)$ since the backing HashMap is unordered.

Equations

• One or more equations did not get rendered due to their size.

def Data.IntMap.lookupMax {v : Type u} (m : IntMap v) : Option (Nat × v)

The largest key-value pair, or none if the map is empty. $$\text{lookupMax}(m) = \max_{k} \{(k, v) \mid k \mapsto v \in m\}$$ Note: $O(n)$ since the backing HashMap is unordered.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.IntMap.instRepr {v : Type u} [Repr v] : Repr (IntMap v)

Equations

• One or more equations did not get rendered due to their size.