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.

theorem Std.DHashMap.Raw.WF.filterMap {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {f : (a : α) → β a → Option (δ a)} : (Raw.filterMap f m).WF

theorem Std.DHashMap.Raw.WF.map {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {f : (a : α) → β a → δ a} : (Raw.map f m).WF

@[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 = { inner := (Std.DHashMap.Internal.Raw₀.filterMap f ⟨m.inner, ⋯⟩).val, wf := ⋯ }

@[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 = { inner := (Std.DHashMap.Internal.Raw₀.map f ⟨m.inner, ⋯⟩).val, wf := ⋯ }