@[inline]

def Std.HashMap.findEntry? {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (m : HashMap α β) (k : α) : Option (α × β)

Given a key a, returns a key-value pair in the map whose key compares equal to a. Note that the returned key may not be identical to the input, if == ignores some part of the value.

def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.findEntry? "one" = some ("one", 1)
hashMap.findEntry? "three" = none

def Std.HashMap.ofListWith {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (l : List (α × β)) (f : β → β → β) : HashMap α β

Variant of ofList which accepts a function that combines values of duplicated keys.

ofListWith [("one", 1), ("one", 2)] (fun v₁ v₂ => v₁ + v₂) = {"one" => 3}

@[reducible, deprecated LawfulHashable (since := "2025-05-31")]

def Batteries.HashMap.LawfulHashable (α : Type u) [BEq α] [Hashable α] : Prop

Alias of LawfulHashable.

---

The BEq α and Hashable α instances on α are compatible. This means that that a == b implies hash a = hash b.

This is automatic if the BEq instance is lawful.

@[deprecated Std.HashMap (since := "2025-04-09")]

structure Batteries.HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] : Type (max u v)

HashMap α β is a key-value map which stores elements in an array using a hash function to find the values. This allows it to have very good performance for lookups (average O(1) for a perfectly random hash function), but it is not a persistent data structure, meaning that one should take care to use the map linearly when performing updates. Copies are O(n).

• inner : Std.HashMap α β

  The inner Std.HashMap powering the Batteries.HashMap.

@[inline]

def Batteries.mkHashMap {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (capacity : Nat := 0) : HashMap α β

Make a new hash map with the specified capacity.

instance Batteries.HashMap.instInhabited {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] : Inhabited (HashMap α β)

instance Batteries.HashMap.instEmptyCollection {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] : EmptyCollection (HashMap α β)

@[inline]

def Batteries.HashMap.empty {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] : HashMap α β

Make a new empty hash map.

(empty : Batteries.HashMap Int Int).toList = []

@[inline]

def Batteries.HashMap.size {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) : Nat

The number of elements in the hash map.

(ofList [("one", 1), ("two", 2)]).size = 2

@[inline]

def Batteries.HashMap.isEmpty {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) : Bool

Is the map empty?

(empty : Batteries.HashMap Int Int).isEmpty = true
(ofList [("one", 1), ("two", 2)]).isEmpty = false

@[inline]

def Batteries.HashMap.insert {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) (a : α) (b : β) : HashMap α β

Inserts key-value pair a, b into the map. If an element equal to a is already in the map, it is replaced by b.

def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.insert "three" 3 = {"one" => 1, "two" => 2, "three" => 3}
hashMap.insert "two" 0 = {"one" => 1, "two" => 0}

@[inline]

def Batteries.HashMap.insert' {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (m : HashMap α β) (a : α) (b : β) : HashMap α β × Bool

Similar to insert, but also returns a boolean flag indicating whether an existing entry has been replaced with a => b.

def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.insert' "three" 3 = ({"one" => 1, "two" => 2, "three" => 3}, false)
hashMap.insert' "two" 0 = ({"one" => 1, "two" => 0}, true)

@[inline]

def Batteries.HashMap.erase {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) (a : α) : HashMap α β

Removes key a from the map. If it does not exist in the map, the map is returned unchanged.

def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.erase "one" = {"two" => 2}
hashMap.erase "three" = {"one" => 1, "two" => 2}

@[inline]

def Batteries.HashMap.modify {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) (a : α) (f : α → β → β) : HashMap α β

Performs an in-place edit of the value, ensuring that the value is used linearly. The function f is passed the original key of the entry, along with the value in the map.

(ofList [("one", 1), ("two", 2)]).modify "one" (fun _ v => v + 1) = {"one" => 2, "two" => 2}
(ofList [("one", 1), ("two", 2)]).modify "three" (fun _ v => v + 1) = {"one" => 1, "two" => 2}

@[inline]

def Batteries.HashMap.find? {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) (a : α) : Option β

Looks up an element in the map with key a.

def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.find? "one" = some 1
hashMap.find? "three" = none

@[inline]

def Batteries.HashMap.findD {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) (a : α) (b₀ : β) : β

Looks up an element in the map with key a. Returns b₀ if the element is not found.

def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.findD "one" 0 = 1
hashMap.findD "three" 0 = 0

@[inline]

def Batteries.HashMap.find! {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} [Inhabited β] (self : HashMap α β) (a : α) : β

Looks up an element in the map with key a. Panics if the element is not found.

def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.find! "one" = 1
hashMap.find! "three" => panic!

instance Batteries.HashMap.instGetElemOptionTrue {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} : GetElem (HashMap α β) α (Option β) fun (x : HashMap α β) (x : α) => True

@[inline]

def Batteries.HashMap.findEntry? {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (m : HashMap α β) (k : α) : Option (α × β)

Given a key a, returns a key-value pair in the map whose key compares equal to a. Note that the returned key may not be identical to the input, if == ignores some part of the value.

def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.findEntry? "one" = some ("one", 1)
hashMap.findEntry? "three" = none

@[inline]

def Batteries.HashMap.contains {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) (a : α) : Bool

Returns true if the element a is in the map.

def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.contains "one" = true
hashMap.contains "three" = false

@[inline]

def Batteries.HashMap.foldM {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Type u_2 → Type u_2} {δ : Type u_2} {β : Type u_3} [Monad m] (f : δ → α → β → m δ) (init : δ) (self : HashMap α β) : m δ

Folds a monadic function over the elements in the map (in arbitrary order).

def sumEven (sum: Nat) (k : String) (v : Nat) : Except String Nat :=
  if v % 2 == 0 then pure (sum + v) else throw s!"value {v} at key {k} is not even"

foldM sumEven 0 (ofList [("one", 1), ("three", 3)]) =
  Except.error "value 3 at key three is not even"
foldM sumEven 0 (ofList [("two", 2), ("four", 4)]) = Except.ok 6

@[inline]

def Batteries.HashMap.fold {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {δ : Type u_2} {β : Type u_3} (f : δ → α → β → δ) (init : δ) (self : HashMap α β) : δ

Folds a function over the elements in the map (in arbitrary order).

fold (fun sum _ v => sum + v) 0 (ofList [("one", 1), ("two", 2)]) = 3

@[specialize #[]]

def Batteries.HashMap.mergeWithM {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Type (max u_2 u_1) → Type (max u_1 u_2)} {β : Type (max u_2 u_1)} [Monad m] (f : α → β → β → m β) (self other : HashMap α β) : m (HashMap α β)

Combines two hashmaps using a monadic function f to combine two values at a key.

def map1 := ofList [("one", 1), ("two", 2)]
def map2 := ofList [("two", 2), ("three", 3)]
def map3 := ofList [("two", 3), ("three", 3)]
def mergeIfNoConflict? (_ : String) (v₁ v₂ : Nat) : Option Nat :=
  if v₁ != v₂ then none else some v₁


mergeWithM mergeIfNoConflict? map1 map2 = some {"one" => 1, "two" => 2, "three" => 3}
mergeWithM mergeIfNoConflict? map1 map3 = none

@[inline]

def Batteries.HashMap.mergeWith {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (f : α → β → β → β) (self other : HashMap α β) : HashMap α β

Combines two hashmaps using function f to combine two values at a key.

mergeWith (fun _ v₁ v₂ => v₁ + v₂ )
  (ofList [("one", 1), ("two", 2)]) (ofList [("two", 2), ("three", 3)]) =
    {"one" => 1, "two" => 4, "three" => 3}

@[inline]

def Batteries.HashMap.forM {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Type u_2 → Type u_2} {β : Type u_3} [Monad m] (f : α → β → m PUnit) (self : HashMap α β) : m PUnit

Runs a monadic function over the elements in the map (in arbitrary order).

def checkEven (k : String) (v : Nat) : Except String Unit :=
  if v % 2 == 0 then pure () else throw s!"value {v} at key {k} is not even"

forM checkEven (ofList [("one", 1), ("three", 3)]) = Except.error "value 3 at key three is not even"
forM checkEven (ofList [("two", 2), ("four", 4)]) = Except.ok ()

def Batteries.HashMap.toList {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) : List (α × β)

Converts the map into a list of key-value pairs.

open List
(ofList [("one", 1), ("two", 2)]).toList ~ [("one", 1), ("two", 2)]

def Batteries.HashMap.toArray {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) : Array (α × β)

Converts the map into an array of key-value pairs.

open List
(ofList [("one", 1), ("two", 2)]).toArray.data ~ #[("one", 1), ("two", 2)].data

def Batteries.HashMap.numBuckets {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) : Nat

The number of buckets in the hash map.

def Batteries.HashMap.ofList {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (l : List (α × β)) : HashMap α β

Builds a HashMap from a list of key-value pairs. Values of duplicated keys are replaced by their respective last occurrences.

ofList [("one", 1), ("one", 2)] = {"one" => 2}

def Batteries.HashMap.ofListWith {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (l : List (α × β)) (f : β → β → β) : HashMap α β

Variant of ofList which accepts a function that combines values of duplicated keys.

ofListWith [("one", 1), ("one", 2)] (fun v₁ v₂ => v₁ + v₂) = {"one" => 3}