Additional dependent hash map operations #
This file defines the operations map and filterMap on Std.Data.DHashMap.
We currently do not provide lemmas for these functions.
theorem
Std.DHashMap.Raw.WF.filterMap
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Raw α β}
(h : m.WF)
{f : (a : α) → β a → Option (δ a)}
:
(Std.DHashMap.Raw.filterMap f m).WF
theorem
Std.DHashMap.Raw.WF.map
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Raw α β}
(h : m.WF)
{f : (a : α) → β a → δ a}
:
(Std.DHashMap.Raw.map f m).WF
@[inline]
def
Std.DHashMap.filterMap
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
[BEq α]
[Hashable α]
(f : (a : α) → β a → Option (δ a))
(m : Std.DHashMap α β)
:
Std.DHashMap α δ
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.DHashMap.filterMap f m = ⟨(Std.DHashMap.Internal.Raw₀.filterMap f ⟨m.val, ⋯⟩).val, ⋯⟩
Instances For
@[inline]
def
Std.DHashMap.map
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
[BEq α]
[Hashable α]
(f : (a : α) → β a → δ a)
(m : Std.DHashMap α β)
:
Std.DHashMap α δ
Updates the values of the hash map by applying the given function to all mappings.
Equations
- Std.DHashMap.map f m = ⟨(Std.DHashMap.Internal.Raw₀.map f ⟨m.val, ⋯⟩).val, ⋯⟩