# Additional dependent raw tree map operations #

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

source
def Std.DTreeMap.Raw.instCoeTypeForall {α : Type u} :
Coe (Type v) (α → Type v)
Equations

- Std.DTreeMap.Raw.instCoeTypeForall = { coe := fun (γ : Type ?u.10) (x : α) => γ }

Instances For

source
@[inline]
def Std.DTreeMap.Raw.filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} (f : (a : α) → β a → Option (γ a)) (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.DTreeMap.Raw.filterMap f t = { inner := Std.DTreeMap.Internal.Impl.filterMap! f t.inner }

Instances For

source
@[inline]
def Std.DTreeMap.Raw.map {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} (f : (a : α) → β a → γ a) (t : Raw α β cmp) :
Raw α γ cmp

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

Equations

- Std.DTreeMap.Raw.map f t = { inner := Std.DTreeMap.Internal.Impl.map f t.inner }

Instances For

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