Documentation

Std.Lean.HashMap

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.
@[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.
@[inline]
def Lean.HashMap.mergeWith {α : Type u_1} [inst : BEq α] [inst : Hashable α] {β : Type u_2} (f : αβββ) (self : Lean.HashMap α β) (other : 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.