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 }

@[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.