Additional dependent raw tree map operations

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

@[instance_reducible]

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

Equations

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

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

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

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