ink

instance Lean.HashMap.instForInHashMapProd {α : Type u_1} [inst : BEq α] [inst : 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.

ink

@[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 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.

ink

@[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 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.