@[specialize #[]]

def
Lean.HashMap.mergeWithM
{m : Type (maxu_1u_2) → Type (maxu_2u_1)}
{α : Type u_2}
{β : Type (maxu_1u_2)}
[inst : BEq α]
[inst : Hashable α]
[inst : Monad m]
(f : α → β → β → m β)
(self : Lean.HashMap α β)
(other : Lean.HashMap α β)
:

m (Lean.HashMap α β)

`O(|other|)`

amortized. Merge two `HashMap`

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.

@[inline]

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

Lean.HashMap α β

`O(|other|)`

amortized. Merge two `HashMap`

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.