# Dependent hash maps #

This file develops the type `Std.DHashMap` of dependent hash maps.

The operations `map` and `filterMap` on `Std.Data.DHashMap` are defined in the module `Std.Data.DHashMap.AdditionalOperations`.

Lemmas about the operations on `Std.Data.DHashMap` are available in the module `Std.Data.DHashMap.Lemmas`.

See the module `Std.Data.DHashMap.Raw` for a variant of this type which is safe to use in nested inductive types and the module `Std.Data.ExtDHashMap` for a variant with extensionality.

For implementation notes, see the docstring of the module `Std.Data.DHashMap.Internal.Defs`.

source
structure Std.DHashMap (α : Type u) (β : α → Type v) [BEq α] [Hashable α] :
Type (max u v)

Dependent hash maps.

This is a simple separate-chaining hash table. The data of the hash map consists of a cached size and an array of buckets, where each bucket is a linked list of key-value pairs. The number of buckets is always a power of two. The hash map doubles its size upon inserting an element such that the number of elements is more than 75% of the number of buckets.

The hash table is backed by an `Array`. Users should make sure that the hash map is used linearly to avoid expensive copies.

The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==` should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the `EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq instance is lawful, i.e., if `a == b` implies `a = b`.

These hash maps contain a bundled well-formedness invariant, which means that they cannot be used in nested inductive types. For these use cases, `Std.DHashMap.Raw` and `Std.DHashMap.Raw.WF` unbundle the invariant from the hash map. When in doubt, prefer `DHashMap` over `DHashMap.Raw`.

For a variant that is more convenient for use in proofs because of extensionalities, see `Std.ExtDHashMap` which is defined in the module `Std.Data.ExtDHashMap`.

- inner : Raw α β

  Internal implementation detail of the hash map.

- wf : self.inner.WF

  Internal implementation detail of the hash map.

Instances For

source
@[inline]
def Std.DHashMap.emptyWithCapacity {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (capacity : Nat := 8) :
DHashMap α β

Creates a new empty hash map. The optional parameter `capacity` can be supplied to presize the map so that it can hold the given number of mappings without reallocating. It is also possible to use the empty collection notations `∅` and `{}` to create an empty hash map with the default capacity.

Equations

- Std.DHashMap.emptyWithCapacity capacity = { inner := Std.DHashMap.Raw.emptyWithCapacity capacity, wf := ⋯ }

Instances For

source
@[reducible, inline, deprecated Std.DHashMap.emptyWithCapacity (since := "2025-03-12")]
abbrev Std.DHashMap.empty {α : Type u_1} {β : α → Type u_2} [BEq α] [Hashable α] (capacity : Nat := 8) :
DHashMap α β

Creates a new empty hash map. The optional parameter `capacity` can be supplied to presize the map so that it can hold the given number of mappings without reallocating. It is also possible to use the empty collection notations `∅` and `{}` to create an empty hash map with the default capacity.

Equations

- @Std.DHashMap.empty = @Std.DHashMap.emptyWithCapacity

Instances For

source
instance Std.DHashMap.instEmptyCollection {α : Type u} {β : α → Type v} [BEq α] [Hashable α] :
EmptyCollection (DHashMap α β)
Equations

- Std.DHashMap.instEmptyCollection = { emptyCollection := Std.DHashMap.emptyWithCapacity }

source
instance Std.DHashMap.instInhabited {α : Type u} {β : α → Type v} [BEq α] [Hashable α] :
Inhabited (DHashMap α β)
Equations

- Std.DHashMap.instInhabited = { default := ∅ }

source
structure Std.DHashMap.Equiv {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m₁ m₂ : DHashMap α β) :
Prop

Two hash maps are equivalent in the sense of `Equiv` iff all the keys and values are equal.

- inner : m₁.inner.Equiv m₂.inner

  Internal implementation detail of the hash map

Instances For

source
def Std.DHashMap.«term_~m_» :
Lean.TrailingParserDescr

Two hash maps are equivalent in the sense of `Equiv` iff all the keys and values are equal.

Equations

- Std.DHashMap.«term_~m_» = Lean.ParserDescr.trailingNode `Std.DHashMap.«term_~m_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~m ") (Lean.ParserDescr.cat `term 51))

Instances For

source
@[inline]
def Std.DHashMap.insert {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : DHashMap α β) (a : α) (b : β a) :
DHashMap α β

Inserts the given mapping into the map. If there is already a mapping for the given key, then both key and value will be replaced.

Note: this replacement behavior is true for `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw`. The `insert` function on `HashSet` and `HashSet.Raw` behaves differently: it will return the set unchanged if a matching key is already present.

Equations

- m.insert a b = { inner := (Std.DHashMap.Internal.Raw₀.insert ⟨m.inner, ⋯⟩ a b).val, wf := ⋯ }

Instances For

source
instance Std.DHashMap.instSingletonSigma {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} :
Singleton ((a : α) × β a) (DHashMap α β)
Equations

- Std.DHashMap.instSingletonSigma = { singleton := fun (x : (a : α) × β a) => match x with | ⟨a, b⟩ => ∅.insert a b }

source
instance Std.DHashMap.instInsertSigma {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} :
Insert ((a : α) × β a) (DHashMap α β)
Equations

- Std.DHashMap.instInsertSigma = { insert := fun (x : (a : α) × β a) (s : Std.DHashMap α β) => match x with | ⟨a, b⟩ => s.insert a b }

source
instance Std.DHashMap.instLawfulSingletonSigma {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} :
LawfulSingleton ((a : α) × β a) (DHashMap α β)
source
@[inline]
def Std.DHashMap.insertIfNew {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : DHashMap α β) (a : α) (b : β a) :
DHashMap α β

If there is no mapping for the given key, inserts the given mapping into the map. Otherwise, returns the map unaltered.

Equations

- m.insertIfNew a b = { inner := (Std.DHashMap.Internal.Raw₀.insertIfNew ⟨m.inner, ⋯⟩ a b).val, wf := ⋯ }

Instances For

source
@[inline]
def Std.DHashMap.containsThenInsert {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : DHashMap α β) (a : α) (b : β a) :
Bool × DHashMap α β

Checks whether a key is present in a map, and unconditionally inserts a value for the key.

Equivalent to (but potentially faster than) calling `contains` followed by `insert`.

Equations

- m.containsThenInsert a b = ((Std.DHashMap.Internal.Raw₀.containsThenInsert ⟨m.inner, ⋯⟩ a b).fst, { inner := (Std.DHashMap.Internal.Raw₀.containsThenInsert ⟨m.inner, ⋯⟩ a b).snd.val, wf := ⋯ })

Instances For

source
@[inline]
def Std.DHashMap.containsThenInsertIfNew {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : DHashMap α β) (a : α) (b : β a) :
Bool × DHashMap α β

Checks whether a key is present in a map and inserts a value for the key if it was not found.

If the returned `Bool` is `true`, then the returned map is unaltered. If the `Bool` is `false`, then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `contains` followed by `insertIfNew`.

Equations

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

Instances For

source
@[inline]
def Std.DHashMap.getThenInsertIfNew? {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] (m : DHashMap α β) (a : α) (b : β a) :
Option (β a) × DHashMap α β

Checks whether a key is present in a map, returning the associated value, and inserts a value for the key if it was not found.

If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.

Uses the `LawfulBEq` instance to cast the retrieved value to the correct type.

Equations

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

Instances For

source
@[inline]
def Std.DHashMap.get? {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] (m : DHashMap α β) (a : α) :
Option (β a)

Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.

Uses the `LawfulBEq` instance to cast the retrieved value to the correct type.

Equations

- m.get? a = Std.DHashMap.Internal.Raw₀.get? ⟨m.inner, ⋯⟩ a

Instances For

source
@[inline]
def Std.DHashMap.contains {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : DHashMap α β) (a : α) :
Bool

Returns `true` if there is a mapping for the given key. There is also a `Prop`-valued version of this: `a ∈ m` is equivalent to `m.contains a = true`.

Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` uses `==` for comparisons, while for hash maps, both use `==`.

Equations

- m.contains a = Std.DHashMap.Internal.Raw₀.contains ⟨m.inner, ⋯⟩ a

Instances For

source
instance Std.DHashMap.instMembership {α : Type u} {β : α → Type v} [BEq α] [Hashable α] :
Membership α (DHashMap α β)
Equations

- Std.DHashMap.instMembership = { mem := fun (m : Std.DHashMap α β) (a : α) => m.contains a = true }

source
instance Std.DHashMap.instDecidableMem {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : DHashMap α β} {a : α} :
Decidable (a ∈ m)
Equations

- Std.DHashMap.instDecidableMem = inferInstanceAs (Decidable (m.contains a = true))

source
@[inline]
def Std.DHashMap.get {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] (m : DHashMap α β) (a : α) (h : a ∈ m) :
β a

Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of `a ∈ m`.

Uses the `LawfulBEq` instance to cast the retrieved value to the correct type.

Equations

- m.get a h = Std.DHashMap.Internal.Raw₀.get ⟨m.inner, ⋯⟩ a h

Instances For

source
@[inline]
def Std.DHashMap.get! {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] (m : DHashMap α β) (a : α) [Inhabited (β a)] :
β a

Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Uses the `LawfulBEq` instance to cast the retrieved value to the correct type.

Equations

- m.get! a = Std.DHashMap.Internal.Raw₀.get! ⟨m.inner, ⋯⟩ a

Instances For

source
@[inline]
def Std.DHashMap.getD {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] (m : DHashMap α β) (a : α) (fallback : β a) :
β a

Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.

Uses the `LawfulBEq` instance to cast the retrieved value to the correct type.

Equations

- m.getD a fallback = Std.DHashMap.Internal.Raw₀.getD ⟨m.inner, ⋯⟩ a fallback

Instances For

source
@[inline]
def Std.DHashMap.erase {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : DHashMap α β) (a : α) :
DHashMap α β

Removes the mapping for the given key if it exists.

Equations

- m.erase a = { inner := (Std.DHashMap.Internal.Raw₀.erase ⟨m.inner, ⋯⟩ a).val, wf := ⋯ }

Instances For

source
@[inline]
def Std.DHashMap.Const.get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} (m : DHashMap α fun (x : α) => β) (a : α) :
Option β

Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.

Equations

- Std.DHashMap.Const.get? m a = Std.DHashMap.Internal.Raw₀.Const.get? ⟨m.inner, ⋯⟩ a

Instances For

source
@[inline]
def Std.DHashMap.Const.get {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} (m : DHashMap α fun (x : α) => β) (a : α) (h : a ∈ m) :
β

Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of `a ∈ m`.

Equations

- Std.DHashMap.Const.get m a h = Std.DHashMap.Internal.Raw₀.Const.get ⟨m.inner, ⋯⟩ a h

Instances For

source
@[inline]
def Std.DHashMap.Const.getD {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} (m : DHashMap α fun (x : α) => β) (a : α) (fallback : β) :
β

Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.

Equations

- Std.DHashMap.Const.getD m a fallback = Std.DHashMap.Internal.Raw₀.Const.getD ⟨m.inner, ⋯⟩ a fallback

Instances For

source
@[inline]
def Std.DHashMap.Const.get! {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [Inhabited β] (m : DHashMap α fun (x : α) => β) (a : α) :
β

Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Equations

- Std.DHashMap.Const.get! m a = Std.DHashMap.Internal.Raw₀.Const.get! ⟨m.inner, ⋯⟩ a

Instances For

source
@[inline]
def Std.DHashMap.Const.getThenInsertIfNew? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} (m : DHashMap α fun (x : α) => β) (a : α) (b : β) :
Option β × DHashMap α fun (x : α) => β

Equivalent to (but potentially faster than) calling `Const.get?` followed by `insertIfNew`.

Checks whether a key is present in a map, returning the associated value, and inserts a value for the key if it was not found.

If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the returned map has a new value inserted.

Equations

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

Instances For

source
@[inline]
def Std.DHashMap.getKey? {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : DHashMap α β) (a : α) :
Option α

Checks if a mapping for the given key exists and returns the key if it does, otherwise `none`. The result in the `some` case is guaranteed to be pointer equal to the key in the map.

Equations

- m.getKey? a = Std.DHashMap.Internal.Raw₀.getKey? ⟨m.inner, ⋯⟩ a

Instances For

source
@[inline]
def Std.DHashMap.getKey {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : DHashMap α β) (a : α) (h : a ∈ m) :
α

Retrieves the key from the mapping that matches `a`. Ensures that such a mapping exists by requiring a proof of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the map.

Equations

- m.getKey a h = Std.DHashMap.Internal.Raw₀.getKey ⟨m.inner, ⋯⟩ a h

Instances For

source
@[inline]
def Std.DHashMap.getKey! {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [Inhabited α] (m : DHashMap α β) (a : α) :
α

Checks if a mapping for the given key exists and returns the key if it does, otherwise panics. If no panic occurs the result is guaranteed to be pointer equal to the key in the map.

Equations

- m.getKey! a = Std.DHashMap.Internal.Raw₀.getKey! ⟨m.inner, ⋯⟩ a

Instances For

source
@[inline]
def Std.DHashMap.getKeyD {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : DHashMap α β) (a fallback : α) :
α

Checks if a mapping for the given key exists and returns the key if it does, otherwise `fallback`. If a mapping exists the result is guaranteed to be pointer equal to the key in the map.

Equations

- m.getKeyD a fallback = Std.DHashMap.Internal.Raw₀.getKeyD ⟨m.inner, ⋯⟩ a fallback

Instances For

source
@[inline]
def Std.DHashMap.size {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : DHashMap α β) :
Nat

The number of mappings present in the hash map

Equations

- m.size = m.inner.size

Instances For

source
@[inline]
def Std.DHashMap.isEmpty {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : DHashMap α β) :
Bool

Returns `true` if the hash map contains no mappings.

Note that if your `BEq` instance is not reflexive or your `Hashable` instance is not lawful, then it is possible that this function returns `false` even though is not possible to get anything out of the hash map.

Equations

- m.isEmpty = m.inner.isEmpty

Instances For

source
@[inline]
def Std.DHashMap.keys {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : DHashMap α β) :
List α

Returns a list of all keys present in the hash map in some order.

Equations

- m.keys = m.inner.keys

Instances For

source
@[inline]
def Std.DHashMap.toList {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : DHashMap α β) :
List ((a : α) × β a)

Transforms the hash map into a list of mappings in some order.

Equations

- m.toList = m.inner.toList

Instances For

source
@[inline]
def Std.DHashMap.Const.toList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} (m : DHashMap α fun (x : α) => β) :
List (α × β)

Transforms the hash map into a list of mappings in some order.

Equations

- Std.DHashMap.Const.toList m = Std.DHashMap.Raw.Const.toList m.inner

Instances For

source
@[inline]
def Std.DHashMap.foldM {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [Monad m] {x✝ : BEq α} {x✝¹ : Hashable α} (f : δ → (a : α) → β a → m δ) (init : δ) (b : DHashMap α β) :
m δ

Monadically computes a value by folding the given function over the mappings in the hash map in some order.

Equations

- Std.DHashMap.foldM f init b = Std.DHashMap.Raw.foldM f init b.inner

Instances For

source
@[inline]
def Std.DHashMap.fold {α : Type u} {β : α → Type v} {δ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} (f : δ → (a : α) → β a → δ) (init : δ) (b : DHashMap α β) :
δ

Folds the given function over the mappings in the hash map in some order.

Equations

- Std.DHashMap.fold f init b = Std.DHashMap.Raw.fold f init b.inner

Instances For

source
@[inline]
def Std.DHashMap.forM {α : Type u} {β : α → Type v} {m : Type w → Type w'} [Monad m] {x✝ : BEq α} {x✝¹ : Hashable α} (f : (a : α) → β a → m PUnit) (b : DHashMap α β) :
m PUnit

Carries out a monadic action on each mapping in the hash map in some order.

Equations

- Std.DHashMap.forM f b = Std.DHashMap.Raw.forM f b.inner

Instances For

source
@[inline]
def Std.DHashMap.forIn {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [Monad m] {x✝ : BEq α} {x✝¹ : Hashable α} (f : (a : α) → β a → δ → m (ForInStep δ)) (init : δ) (b : DHashMap α β) :
m δ

Support for the `for` loop construct in `do` blocks.

Equations

- Std.DHashMap.forIn f init b = Std.DHashMap.Raw.forIn f init b.inner

Instances For

source
instance Std.DHashMap.instForMSigma {α : Type u} {β : α → Type v} {m : Type w → Type w'} [BEq α] [Hashable α] :
ForM m (DHashMap α β) ((a : α) × β a)
Equations

- Std.DHashMap.instForMSigma = { forM := fun [Monad m] (m_1 : Std.DHashMap α β) (f : (a : α) × β a → m PUnit) => Std.DHashMap.forM (fun (a : α) (b : β a) => f ⟨a, b⟩) m_1 }

source
instance Std.DHashMap.instForInSigma {α : Type u} {β : α → Type v} {m : Type w → Type w'} [BEq α] [Hashable α] :
ForIn m (DHashMap α β) ((a : α) × β a)
Equations

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

We do not define `ForM` and `ForIn` instances that are specialized to constant `β`. Instead, we define uncurried versions of `forM` and `forIn` that will be used in the `Const` lemmas and to define the `ForM` and `ForIn` instances for `HashMap`.

source
@[inline]
def Std.DHashMap.Const.forMUncurried {α : Type u} {m : Type w → Type w'} [Monad m] {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} (f : α × β → m PUnit) (b : DHashMap α fun (x : α) => β) :
m PUnit

Carries out a monadic action on each mapping in the hash map in some order.

Equations

- Std.DHashMap.Const.forMUncurried f b = Std.DHashMap.forM (fun (a : α) (b : β) => f (a, b)) b

Instances For

source
@[inline]
def Std.DHashMap.Const.forInUncurried {α : Type u} {δ : Type w} {m : Type w → Type w'} [Monad m] {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} (f : α × β → δ → m (ForInStep δ)) (init : δ) (b : DHashMap α fun (x : α) => β) :
m δ

Support for the `for` loop construct in `do` blocks.

Equations

- Std.DHashMap.Const.forInUncurried f init b = Std.DHashMap.forIn (fun (a : α) (b : β) (d : δ) => f (a, b) d) init b

Instances For

source
@[inline]
def Std.DHashMap.filter {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (f : (a : α) → β a → Bool) (m : DHashMap α β) :
DHashMap α β

Removes all mappings of the hash map for which the given function returns `false`.

Equations

- Std.DHashMap.filter f m = { inner := (Std.DHashMap.Internal.Raw₀.filter f ⟨m.inner, ⋯⟩).val, wf := ⋯ }

Instances For

source
@[inline]
def Std.DHashMap.modify {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] (m : DHashMap α β) (a : α) (f : β a → β a) :
DHashMap α β

Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.

Equations

- m.modify a f = { inner := (Std.DHashMap.Internal.Raw₀.modify ⟨m.inner, ⋯⟩ a f).val, wf := ⋯ }

Instances For

source
@[inline]
def Std.DHashMap.Const.modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} (m : DHashMap α fun (x : α) => β) (a : α) (f : β → β) :
DHashMap α fun (x : α) => β

Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.

Equations

- Std.DHashMap.Const.modify m a f = { inner := (Std.DHashMap.Internal.Raw₀.Const.modify ⟨m.inner, ⋯⟩ a f).val, wf := ⋯ }

Instances For

source
@[inline]
def Std.DHashMap.alter {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] (m : DHashMap α β) (a : α) (f : Option (β a) → Option (β a)) :
DHashMap α β

Modifies in place the value associated with a given key, allowing creating new values and deleting values via an `Option` valued replacement function.

This function ensures that the value is used linearly.

Equations

- m.alter a f = { inner := (Std.DHashMap.Internal.Raw₀.alter ⟨m.inner, ⋯⟩ a f).val, wf := ⋯ }

Instances For

source
@[inline]
def Std.DHashMap.Const.alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} (m : DHashMap α fun (x : α) => β) (a : α) (f : Option β → Option β) :
DHashMap α fun (x : α) => β

Modifies in place the value associated with a given key, allowing creating new values and deleting values via an `Option` valued replacement function.

This function ensures that the value is used linearly.

Equations

- Std.DHashMap.Const.alter m a f = { inner := (Std.DHashMap.Internal.Raw₀.Const.alter ⟨m.inner, ⋯⟩ a f).val, wf := ⋯ }

Instances For

source
@[inline]
def Std.DHashMap.insertMany {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] (m : DHashMap α β) (l : ρ) :
DHashMap α β

Inserts multiple mappings into the hash map by iterating over the given collection and calling `insert`. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw`. The `insertMany` function on `HashSet` and `HashSet.Raw` behaves differently: it will prefer the first appearance.

Equations

- m.insertMany l = { inner := (Std.DHashMap.Internal.Raw₀.insertMany ⟨m.inner, ⋯⟩ l).val.val, wf := ⋯ }

Instances For

source
@[inline]
def Std.DHashMap.Const.insertMany {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {ρ : Type w} [ForIn Id ρ (α × β)] (m : DHashMap α fun (x : α) => β) (l : ρ) :
DHashMap α fun (x : α) => β

Inserts multiple mappings into the hash map by iterating over the given collection and calling `insert`. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw`. The `insertMany` function on `HashSet` and `HashSet.Raw` behaves differently: it will prefer the first appearance.

Equations

- Std.DHashMap.Const.insertMany m l = { inner := (Std.DHashMap.Internal.Raw₀.Const.insertMany ⟨m.inner, ⋯⟩ l).val.val, wf := ⋯ }

Instances For

source
@[inline]
def Std.DHashMap.Const.insertManyIfNewUnit {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {ρ : Type w} [ForIn Id ρ α] (m : DHashMap α fun (x : α) => Unit) (l : ρ) :
DHashMap α fun (x : α) => Unit

Inserts multiple keys with the value `()` into the hash map by iterating over the given collection and calling `insertIfNew`. If the same key appears multiple times, the first occurrence takes precedence.

This is mainly useful to implement `HashSet.insertMany`, so if you are considering using this, `HashSet` or `HashSet.Raw` might be a better fit for you.

Equations

- Std.DHashMap.Const.insertManyIfNewUnit m l = { inner := (Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit ⟨m.inner, ⋯⟩ l).val.val, wf := ⋯ }

Instances For

source
@[inline]
def Std.DHashMap.toArray {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : DHashMap α β) :
Array ((a : α) × β a)

Transforms the hash map into an array of mappings in some order.

Equations

- m.toArray = m.inner.toArray

Instances For

source
@[inline]
def Std.DHashMap.Const.toArray {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} (m : DHashMap α fun (x : α) => β) :
Array (α × β)

Transforms the hash map into an array of mappings in some order.

Equations

- Std.DHashMap.Const.toArray m = Std.DHashMap.Raw.Const.toArray m.inner

Instances For

source
@[inline]
def Std.DHashMap.keysArray {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : DHashMap α β) :
Array α

Returns an array of all keys present in the hash map in some order.

Equations

- m.keysArray = m.inner.keysArray

Instances For

source
@[inline]
def Std.DHashMap.union {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m₁ m₂ : DHashMap α β) :
DHashMap α β

Computes the union of the given hash maps. If a key appears in both maps, the entry contains in the second argument will appear in the result.

This function always merges the smaller map into the larger map, so the expected runtime is `O(min(m₁.size, m₂.size))`.

Equations

- m₁.union m₂ = { inner := (Std.DHashMap.Internal.Raw₀.union ⟨m₁.inner, ⋯⟩ ⟨m₂.inner, ⋯⟩).val, wf := ⋯ }

Instances For

source
instance Std.DHashMap.instUnion {α : Type u} {β : α → Type v} [BEq α] [Hashable α] :
Union (DHashMap α β)
Equations

- Std.DHashMap.instUnion = { union := Std.DHashMap.union }

We currently do not provide lemmas for the functions below.

source
@[inline]
def Std.DHashMap.partition {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (f : (a : α) → β a → Bool) (m : DHashMap α β) :
DHashMap α β × DHashMap α β

Partition a hash map into two hash map based on a predicate.

Equations

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

Instances For

source
@[inline]
def Std.DHashMap.values {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} (m : DHashMap α fun (x : α) => β) :
List β

Returns a list of all values present in the hash map in some order.

Equations

- m.values = m.inner.values

Instances For

source
@[inline]
def Std.DHashMap.valuesArray {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} (m : DHashMap α fun (x : α) => β) :
Array β

Returns an array of all values present in the hash map in some order.

Equations

- m.valuesArray = m.inner.valuesArray

Instances For

source
@[inline]
def Std.DHashMap.Const.unitOfArray {α : Type u} [BEq α] [Hashable α] (l : Array α) :
DHashMap α fun (x : α) => Unit

Creates a hash map from an array of keys, associating the value `()` with each key.

This is mainly useful to implement `HashSet.ofArray`, so if you are considering using this, `HashSet` or `HashSet.Raw` might be a better fit for you.

Equations

- Std.DHashMap.Const.unitOfArray l = Std.DHashMap.Const.insertManyIfNewUnit ∅ l

Instances For

source
def Std.DHashMap.Internal.numBuckets {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : DHashMap α β) :
Nat

Returns the number of buckets in the internal representation of the hash map. This function may be useful for things like monitoring system health, but it should be considered an internal implementation detail.

Equations

- Std.DHashMap.Internal.numBuckets m = Std.DHashMap.Raw.Internal.numBuckets m.inner

Instances For

source
instance Std.DHashMap.instRepr {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [Repr α] [(a : α) → Repr (β a)] :
Repr (DHashMap α β)
Equations

- Std.DHashMap.instRepr = { reprPrec := fun (m : Std.DHashMap α β) (prec : Nat) => Repr.addAppParen (Std.Format.text "Std.DHashMap.ofList " ++ reprArg m.toList) prec }

source
@[inline]
def Std.DHashMap.ofList {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (l : List ((a : α) × β a)) :
DHashMap α β

Creates a hash map from a list of mappings. If the same key appears multiple times, the last occurrence takes precedence.

Equations

- Std.DHashMap.ofList l = ∅.insertMany l

Instances For

source
@[inline]
def Std.DHashMap.Const.ofList {α : Type u} {β : Type v} [BEq α] [Hashable α] (l : List (α × β)) :
DHashMap α fun (x : α) => β

Creates a hash map from a list of mappings. If the same key appears multiple times, the last occurrence takes precedence.

Equations

- Std.DHashMap.Const.ofList l = Std.DHashMap.Const.insertMany ∅ l

Instances For

source
@[inline]
def Std.DHashMap.Const.unitOfList {α : Type u} [BEq α] [Hashable α] (l : List α) :
DHashMap α fun (x : α) => Unit

Creates a hash map from a list of keys, associating the value `()` with each key.

This is mainly useful to implement `HashSet.ofList`, so if you are considering using this, `HashSet` or `HashSet.Raw` might be a better fit for you.

Equations

- Std.DHashMap.Const.unitOfList l = Std.DHashMap.Const.insertManyIfNewUnit ∅ l

Instances For