@[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 other : PersistentHashMap α β)
(f : α → β → β → m β)
:
m (PersistentHashMap α β)
Merge two PersistentHashMap
s. The values of keys which appear in both maps are
combined using the monadic function f
.
Equations
Instances For
@[inline]
def
Lean.PersistentHashMap.mergeWith
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
(self other : PersistentHashMap α β)
(f : α → β → β → β)
:
Merge two PersistentHashMap
s. The values of keys which appear in both maps are
combined using f
.