def
Lean.PersistentHashMap.ofList
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
(xs : List (α × β))
:

Builds a `PersistentHashMap`

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

## Equations

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

## Instances For

def
Lean.PersistentHashMap.ofArray
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
(xs : Array (α × β))
:

Builds a `PersistentHashMap`

from an array of key-value pairs. Values of
duplicated keys are replaced by their respective last occurrences.

## Equations

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

## Instances For

@[specialize #[]]

def
Lean.PersistentHashMap.mergeWithM
{α : Type u_1}
[BEq α]
[Hashable α]
{m : Type (max u_2 u_1) → Type u_3}
{β : Type (max u_2 u_1)}
[Monad m]
(self : Lean.PersistentHashMap α β)
(other : Lean.PersistentHashMap α β)
(f : α → β → β → m β)
:

m (Lean.PersistentHashMap α β)

Merge two `PersistentHashMap`

s. The values of keys which appear in both maps are
combined using the monadic function `f`

.

## Equations

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

## Instances For

@[inline]

def
Lean.PersistentHashMap.mergeWith
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
(self : Lean.PersistentHashMap α β)
(other : Lean.PersistentHashMap α β)
(f : α → β → β → β)
:

Merge two `PersistentHashMap`

s. The values of keys which appear in both maps are
combined using `f`

.

## Equations

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