Additional dependent tree map operations

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

@[inline]

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

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

@[inline]

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

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.DTreeMap.getEntryGT {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : DTreeMap α β cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ cmp a k = Ordering.gt) : (a : α) × β a

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.DTreeMap.getEntryLE {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : DTreeMap α β cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ (cmp a k).isLE = true) : (a : α) × β a

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.DTreeMap.getEntryLT {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : DTreeMap α β cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ cmp a k = Ordering.lt) : (a : α) × β a

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.DTreeMap.getKeyGE {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : DTreeMap α β 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.DTreeMap.getKeyGT {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : DTreeMap α β 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.DTreeMap.getKeyLE {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : DTreeMap α β 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.DTreeMap.getKeyLT {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : DTreeMap α β 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.

@[inline]

def Std.DTreeMap.Const.getEntryGE {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : DTreeMap α (fun (x : α) => β) 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.DTreeMap.Const.getEntryGT {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : DTreeMap α (fun (x : α) => β) 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.DTreeMap.Const.getEntryLE {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : DTreeMap α (fun (x : α) => β) 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.DTreeMap.Const.getEntryLT {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : DTreeMap α (fun (x : α) => β) 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.