Additional dependent hash map operations #
This file defines the operations map
and filterMap
on Std.DHashMap
.
Lemmas about these operations are found in Std.Data.DHashMap.Lemmas
.
@[inline]
def
Std.DHashMap.filterMap
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
[BEq α]
[Hashable α]
(f : (a : α) → β a → Option (δ a))
(m : DHashMap α β)
:
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 : DHashMap α β)
:
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, ⋯⟩