Additional raw tree map operations

This file defines more operations on Std.TreeMap.Raw. We currently do not provide lemmas for these functions.

@[inline]

def Std.TreeMap.Raw.filterMap {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} (f : α → β → Option γ) (t : Raw α β cmp) : Raw α γ cmp

Updates the values of the map by applying the given function to all mappings, keeping only those mappings where the function returns some value.

Equations

• Std.TreeMap.Raw.filterMap f t = { inner := Std.DTreeMap.Raw.filterMap f t.inner }

@[inline]

def Std.TreeMap.Raw.map {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} (f : α → β → γ) (t : Raw α β cmp) : Raw α γ cmp

Updates the values of the map by applying the given function to all mappings.

Equations

• Std.TreeMap.Raw.map f t = { inner := Std.DTreeMap.Raw.map f t.inner }

We do not provide get*GE, get*GT, get*LE and get*LT functions for the raw trees.