instance Lean.HashMap.instForInHashMapProd {α : Type u_1} [BEq α] [Hashable α] {m : Type u_2 → Type u_2} {β : Type u_3} : ForIn m (Lean.HashMap α β) (α × β)

Equations

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

@[specialize #[]]

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

O(|other|) amortized. Merge two HashMaps. 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} [BEq α] [Hashable α] {β : Type u_2} (f : α → β → β → β) (self : Lean.HashMap α β) (other : Lean.HashMap α β) : Lean.HashMap α β

O(|other|) amortized. Merge two HashMaps. 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.