Convenience functions for hash maps #
These will be reimplemented in the Lean standard library.
def
Std.HashMap.mapVal
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[BEq α]
[Hashable α]
(f : α → β → γ)
(m : Std.HashMap α β)
:
Std.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)) Std.HashMap.empty m