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.

Equations

• Std.DTreeMap.filterMap f t = { inner := (Std.DTreeMap.Internal.Impl.filterMap f t.inner ⋯).impl, wf := ⋯ }

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

Equations

• Std.DTreeMap.map f t = { inner := Std.DTreeMap.Internal.Impl.map f t.inner, wf := ⋯ }

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

Equations

• t.getEntryGE k h = Std.DTreeMap.Internal.Impl.getEntryGE k t.inner ⋯ h

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

Equations

• t.getEntryGT k h = Std.DTreeMap.Internal.Impl.getEntryGT k t.inner ⋯ h

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

Equations

• t.getEntryLE k h = Std.DTreeMap.Internal.Impl.getEntryLE k t.inner ⋯ h

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

Equations

• t.getEntryLT k h = Std.DTreeMap.Internal.Impl.getEntryLT k t.inner ⋯ h

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

Equations

• t.getKeyGE k h = Std.DTreeMap.Internal.Impl.getKeyGE k t.inner ⋯ h

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

Equations

• t.getKeyGT k h = Std.DTreeMap.Internal.Impl.getKeyGT k t.inner ⋯ h

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

Equations

• t.getKeyLE k h = Std.DTreeMap.Internal.Impl.getKeyLE k t.inner ⋯ h

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

Equations

• t.getKeyLT k h = Std.DTreeMap.Internal.Impl.getKeyLT k t.inner ⋯ h

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

Equations

• Std.DTreeMap.Const.getEntryGE t k h = Std.DTreeMap.Internal.Impl.Const.getEntryGE k t.inner ⋯ h

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

Equations

• Std.DTreeMap.Const.getEntryGT t k h = Std.DTreeMap.Internal.Impl.Const.getEntryGT k t.inner ⋯ h

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

Equations

• Std.DTreeMap.Const.getEntryLE t k h = Std.DTreeMap.Internal.Impl.Const.getEntryLE k t.inner ⋯ h

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

Equations

• Std.DTreeMap.Const.getEntryLT t k h = Std.DTreeMap.Internal.Impl.Const.getEntryLT k t.inner ⋯ h