Additional hash map operations

This module defines the operations map and filterMap on Std.HashMap. Lemmas about these operations are found in Std.Data.HashMap.Lemmas.

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

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

@[inline]

def Std.HashMap.filterMap {α : Type u} {β : Type v} {γ : Type w} [BEq α] [Hashable α] (f : α → β → Option γ) (m : HashMap α β) : 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 }

@[inline]

def Std.HashMap.map {α : Type u} {β : Type v} {γ : Type w} [BEq α] [Hashable α] (f : α → β → γ) (m : HashMap α β) : 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 }