Additional tree map operations

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

@[inline]

def Std.TreeMap.filterMap {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} (f : α → β → Option γ) (m : TreeMap α β cmp) : TreeMap α γ 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.filterMap f m = { inner := Std.DTreeMap.filterMap f m.inner }

@[inline]

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

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

Equations

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

@[inline]

def Std.TreeMap.getEntryGE {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : TreeMap α β cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ (cmp a k).isGE = true) : α × β

Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is greater than or equal to the given key.

Equations

• t.getEntryGE k h = Std.DTreeMap.Const.getEntryGE t.inner k h

@[inline]

def Std.TreeMap.getEntryGT {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : TreeMap α β cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ cmp a k = Ordering.gt) : α × β

Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is greater than the given key.

Equations

• t.getEntryGT k h = Std.DTreeMap.Const.getEntryGT t.inner k h

@[inline]

def Std.TreeMap.getEntryLE {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : TreeMap α β cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ (cmp a k).isLE = true) : α × β

Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is less than or equal to the given key.

Equations

• t.getEntryLE k h = Std.DTreeMap.Const.getEntryLE t.inner k h

@[inline]

def Std.TreeMap.getEntryLT {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : TreeMap α β cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ cmp a k = Ordering.lt) : α × β

Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is less than the given key.

Equations

• t.getEntryLT k h = Std.DTreeMap.Const.getEntryLT t.inner k h

@[inline]

def Std.TreeMap.getKeyGE {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : TreeMap α β cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ (cmp a k).isGE = true) : α

Given a proof that such a mapping exists, retrieves the smallest key that is greater than or equal to the given key.

Equations

• t.getKeyGE k h = t.inner.getKeyGE k h

@[inline]

def Std.TreeMap.getKeyGT {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : TreeMap α β cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ cmp a k = Ordering.gt) : α

Given a proof that such a mapping exists, retrieves the smallest key that is greater than the given key.

Equations

• t.getKeyGT k h = t.inner.getKeyGT k h

@[inline]

def Std.TreeMap.getKeyLE {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : TreeMap α β cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ (cmp a k).isLE = true) : α

Given a proof that such a mapping exists, retrieves the largest key that is less than or equal to the given key.

Equations

• t.getKeyLE k h = t.inner.getKeyLE k h

@[inline]

def Std.TreeMap.getKeyLT {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : TreeMap α β cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ cmp a k = Ordering.lt) : α

Given a proof that such a mapping exists, retrieves the smallest key that is less than the given key.

Equations

• t.getKeyLT k h = t.inner.getKeyLT k h