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.

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

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

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

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

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

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

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

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

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