Convenience functions for hash maps #
This is now reimplemented in the Lean standard library.
@[deprecated Std.HashMap.map (since := "2025-08-18")]
def
Std.HashMap.mapVal
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[BEq α]
[Hashable α]
(f : α → β → γ)
(m : HashMap α β)
:
HashMap α γ
Apply a function to the values of a hash map.
Equations
- Std.HashMap.mapVal f m = Std.HashMap.fold (fun (acc : Std.HashMap α γ) (k : α) (v : β) => acc.insert k (f k v)) ∅ m