# 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`.

source
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
source
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
source
@[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 }

Instances For

source
@[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 }

Instances For