Additional hash map operations #
This module defines the operations map and filterMap on Std.Data.HashMap.
We currently do not provide lemmas for these functions.
theorem
Std.HashMap.Raw.WF.filterMap
{α : Type u}
{β : Type v}
{γ : Type w}
[BEq α]
[Hashable α]
{m : Std.HashMap.Raw α β}
{f : α → β → Option γ}
(h : m.WF)
:
(Std.HashMap.Raw.filterMap f m).WF
theorem
Std.HashMap.Raw.WF.map
{α : Type u}
{β : Type v}
{γ : Type w}
[BEq α]
[Hashable α]
{m : Std.HashMap.Raw α β}
{f : α → β → γ}
(h : m.WF)
:
(Std.HashMap.Raw.map f m).WF
@[inline]
def
Std.HashMap.filterMap
{α : Type u}
{β : Type v}
{γ : Type w}
[BEq α]
[Hashable α]
(f : α → β → Option γ)
(m : Std.HashMap α β)
:
Std.HashMap α γ
Updates the values of the hash map by applying the given function to all mappings, keeping
only those mappings where the function returns some value.
Equations
- Std.HashMap.filterMap f m = { inner := Std.DHashMap.filterMap f m.inner }
Instances For
@[inline]
def
Std.HashMap.map
{α : Type u}
{β : Type v}
{γ : Type w}
[BEq α]
[Hashable α]
(f : α → β → γ)
(m : Std.HashMap α β)
:
Std.HashMap α γ
Updates the values of the hash map by applying the given function to all mappings.
Equations
- Std.HashMap.map f m = { inner := Std.DHashMap.map f m.inner }