Low-level implementation of the size-bounded tree

This file contains the basic definition implementing the functionality of the size-bounded trees.

minView and maxView

structure Std.DTreeMap.Internal.Impl.RawView (α : Type u) (β : α → Type v) : Type (max u v)

A tuple of a key-value pair and a tree.

• k : α

  The key.

• v : β self.k

  The value.

• tree : Impl α β

  The tree.

structure Std.DTreeMap.Internal.Impl.Tree (α : Type u) (β : α → Type v) (size : Nat) : Type (max u v)

A balanced tree of the given size.

• impl : Impl α β

  The tree.

• balanced_impl : self.impl.Balanced

  The tree is balanced.

• size_impl : self.impl.size = size

  The tree has size size.

structure Std.DTreeMap.Internal.Impl.View (α : Type u) (β : α → Type v) (size : Nat) : Type (max u v)

A tuple of a key-value pair and a balanced tree of size size.

• k : α

  The key.

• v : β self.k

  The value.

• tree : Tree α β size

  The tree.

def Std.DTreeMap.Internal.Impl.minView {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Impl α β) (hl : l.Balanced) (hr : r.Balanced) (hlr : BalancedAtRoot l.size r.size) : View α β (l.size + r.size)

Returns the tree l ++ ⟨k, v⟩ ++ r, with the smallest element chopped off.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.minView k v Std.DTreeMap.Internal.Impl.leaf r hl_2 hr hlr_2 = { k := k, v := v, tree := { impl := r, balanced_impl := hr, size_impl := ⋯ } }

def Std.DTreeMap.Internal.Impl.minView! {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Impl α β) : RawView α β

Slower version of minView which can be used in the absence of balance information but still assumes the preconditions of minView, otherwise might panic.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.minView! k v Std.DTreeMap.Internal.Impl.leaf r = { k := k, v := v, tree := r }

def Std.DTreeMap.Internal.Impl.maxView {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Impl α β) (hl : l.Balanced) (hr : r.Balanced) (hlr : BalancedAtRoot l.size r.size) : View α β (l.size + r.size)

Returns the tree l ++ ⟨k, v⟩ ++ r, with the largest element chopped off.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.maxView k v l Std.DTreeMap.Internal.Impl.leaf hl hr_2 hlr_2 = { k := k, v := v, tree := { impl := l, balanced_impl := hl, size_impl := ⋯ } }

def Std.DTreeMap.Internal.Impl.maxView! {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Impl α β) : RawView α β

Slower version of maxView which can be used in the absence of balance information but still assumes the preconditions of maxView, otherwise might panic.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.maxView! k v l Std.DTreeMap.Internal.Impl.leaf = { k := k, v := v, tree := l }

glue

@[inline]

def Std.DTreeMap.Internal.Impl.glue {α : Type u} {β : α → Type v} (l r : Impl α β) (hl : l.Balanced) (hr : r.Balanced) (hlr : BalancedAtRoot l.size r.size) : Impl α β

Constructs the tree l ++ r.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.leaf.glue r hl_2 hr hlr_2 = r
• (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').glue Std.DTreeMap.Internal.Impl.leaf hl_2 hr_2 hlr_3 = Std.DTreeMap.Internal.Impl.inner size k' v' l' r'

theorem Std.DTreeMap.Internal.Impl.size_glue {α : Type u} {β : α → Type v} {l r : Impl α β} {hl : l.Balanced} {hr : r.Balanced} {hlr : BalancedAtRoot l.size r.size} : (l.glue r hl hr hlr).size = l.size + r.size

theorem Std.DTreeMap.Internal.Impl.balanced_glue {α : Type u} {β : α → Type v} {l r : Impl α β} {hl : l.Balanced} {hr : r.Balanced} {hlr : BalancedAtRoot l.size r.size} : (l.glue r hl hr hlr).Balanced

@[inline]

def Std.DTreeMap.Internal.Impl.glue! {α : Type u} {β : α → Type v} (l r : Impl α β) : Impl α β

Slower version of glue which can be used in the absence of balance information but still assumes the preconditions of glue, otherwise might panic.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.leaf.glue! r = r
• (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').glue! Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r''

insertMin and insertMax

def Std.DTreeMap.Internal.Impl.insertMin {α : Type u} {β : α → Type v} (k : α) (v : β k) (t : Impl α β) (hr : t.Balanced) : Tree α β (1 + t.size)

Inserts an element at the beginning of the tree.

Equations

• One or more equations did not get rendered due to their size.

def Std.DTreeMap.Internal.Impl.insertMin! {α : Type u} {β : α → Type v} (k : α) (v : β k) (t : Impl α β) : Impl α β

Slower version of insertMin which can be used in the absence of balance information but still assumes the preconditions of insertMin, otherwise might panic.

Equations

• Std.DTreeMap.Internal.Impl.insertMin! k v Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf
• Std.DTreeMap.Internal.Impl.insertMin! k v (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') = Std.DTreeMap.Internal.Impl.balanceL! k' v' (Std.DTreeMap.Internal.Impl.insertMin! k v l') r'

def Std.DTreeMap.Internal.Impl.insertMax {α : Type u} {β : α → Type v} (k : α) (v : β k) (t : Impl α β) (hl : t.Balanced) : Tree α β (t.size + 1)

Inserts an element at the end of the tree.

Equations

• One or more equations did not get rendered due to their size.

def Std.DTreeMap.Internal.Impl.insertMax! {α : Type u} {β : α → Type v} (k : α) (v : β k) (t : Impl α β) : Impl α β

Slower version of insertMax which can be used in the absence of balance information but still assumes the preconditions of insertMax, otherwise might panic.

Equations

• Std.DTreeMap.Internal.Impl.insertMax! k v Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf
• Std.DTreeMap.Internal.Impl.insertMax! k v (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') = Std.DTreeMap.Internal.Impl.balanceR! k' v' l' (Std.DTreeMap.Internal.Impl.insertMax! k v r')

link and link2

@[irreducible]

def Std.DTreeMap.Internal.Impl.link {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Impl α β) (hl : l.Balanced) (hr : r.Balanced) : Tree α β (l.size + 1 + r.size)

Builds the tree l ++ ⟨k, v⟩ ++ r without any balancing information at the root.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.link k v Std.DTreeMap.Internal.Impl.leaf r hr_2 hr = { impl := (Std.DTreeMap.Internal.Impl.insertMin k v r ⋯).impl, balanced_impl := ⋯, size_impl := ⋯ }

@[irreducible]

def Std.DTreeMap.Internal.Impl.link! {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Impl α β) : Impl α β

Slower version of link which can be used in the absence of balance information but still assumes the preconditions of link, otherwise might panic.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.link! k v Std.DTreeMap.Internal.Impl.leaf r = Std.DTreeMap.Internal.Impl.insertMin! k v r

@[irreducible]

def Std.DTreeMap.Internal.Impl.link2 {α : Type u} {β : α → Type v} (l r : Impl α β) (hl : l.Balanced) (hr : r.Balanced) : Tree α β (l.size + r.size)

Builds the tree l ++ r without any balancing information at the root.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.leaf.link2 r hr_2 hr = { impl := r, balanced_impl := ⋯, size_impl := ⋯ }

@[irreducible]

def Std.DTreeMap.Internal.Impl.link2! {α : Type u} {β : α → Type v} (l r : Impl α β) : Impl α β

Slower version of link2 which can be used in the absence of balance information but still assumes the preconditions of link2, otherwise might panic.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.leaf.link2! r = r
• (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').link2! Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r''

Modification operations

structure Std.DTreeMap.Internal.Impl.SizedBalancedTree (α : Type u) (β : α → Type v) (lb ub : Nat) : Type (max u v)

A balanced tree of one of the given sizes.

• impl : Impl α β

  The tree.

• balanced_impl : self.impl.Balanced

  The tree is balanced.

• lb_le_size_impl : lb ≤ self.impl.size

  The tree has size at least lb.

• size_impl_le_ub : self.impl.size ≤ ub

  The tree has size at most ub.

@[inline]

def Std.DTreeMap.Internal.Impl.empty {α : Type u} {β : α → Type v} : Impl α β

An empty tree.

Equations

• Std.DTreeMap.Internal.Impl.empty = Std.DTreeMap.Internal.Impl.leaf

theorem Std.DTreeMap.Internal.Impl.balanced_empty {α : Type u} {β : α → Type v} : empty.Balanced

def Std.DTreeMap.Internal.Impl.insert {α : Type u} {β : α → Type v} [Ord α] (k : α) (v : β k) (t : Impl α β) (hl : t.Balanced) : SizedBalancedTree α β t.size (t.size + 1)

Adds a new mapping to the key, overwriting an existing one with equal key if present.

Equations

• One or more equations did not get rendered due to their size.

def Std.DTreeMap.Internal.Impl.insert! {α : Type u} {β : α → Type v} [Ord α] (k : α) (v : β k) (t : Impl α β) : Impl α β

Slower version of insert which can be used in the absence of balance information but still assumes the preconditions of insert, otherwise might panic.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.insert! k v Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf

@[inline]

def Std.DTreeMap.Internal.Impl.containsThenInsert {α : Type u} {β : α → Type v} [Ord α] (k : α) (v : β k) (t : Impl α β) (hl : t.Balanced) : Bool × SizedBalancedTree α β t.size (t.size + 1)

Returns the pair (t.contains k, t.insert k v).

Equations

• One or more equations did not get rendered due to their size.

def Std.DTreeMap.Internal.Impl.containsThenInsert.size {α : Type u} {β : α → Type v} : Impl α β → Nat

Equations

• Std.DTreeMap.Internal.Impl.containsThenInsert.size Std.DTreeMap.Internal.Impl.leaf = 0
• Std.DTreeMap.Internal.Impl.containsThenInsert.size (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') = size

@[inline]

def Std.DTreeMap.Internal.Impl.containsThenInsert! {α : Type u} {β : α → Type v} [Ord α] (k : α) (v : β k) (t : Impl α β) : Bool × Impl α β

Slower version of containsThenInsert which can be used in the absence of balance information but still assumes the preconditions of containsThenInsert, otherwise might panic.

Equations

• One or more equations did not get rendered due to their size.

def Std.DTreeMap.Internal.Impl.containsThenInsert!.size {α : Type u} {β : α → Type v} : Impl α β → Nat

Equations

• Std.DTreeMap.Internal.Impl.containsThenInsert!.size Std.DTreeMap.Internal.Impl.leaf = 0
• Std.DTreeMap.Internal.Impl.containsThenInsert!.size (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') = size

@[inline]

def Std.DTreeMap.Internal.Impl.insertIfNew {α : Type u} {β : α → Type v} [Ord α] (k : α) (v : β k) (t : Impl α β) (hl : t.Balanced) : SizedBalancedTree α β t.size (t.size + 1)

Adds a new mapping to the tree, leaving the tree unchanged if the key is already present.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.DTreeMap.Internal.Impl.insertIfNew! {α : Type u} {β : α → Type v} [Ord α] (k : α) (v : β k) (t : Impl α β) : Impl α β

Slower version of insertIfNew which can be used in the absence of balance information but still assumes the preconditions of insertIfNew, otherwise might panic.

Equations

• Std.DTreeMap.Internal.Impl.insertIfNew! k v t = if Std.DTreeMap.Internal.Impl.contains k t = true then t else Std.DTreeMap.Internal.Impl.insert! k v t

@[inline]

def Std.DTreeMap.Internal.Impl.containsThenInsertIfNew {α : Type u} {β : α → Type v} [Ord α] (k : α) (v : β k) (t : Impl α β) (hl : t.Balanced) : Bool × SizedBalancedTree α β t.size (t.size + 1)

Returns the pair (t.contains k, t.insertIfNew k v).

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.DTreeMap.Internal.Impl.containsThenInsertIfNew! {α : Type u} {β : α → Type v} [Ord α] (k : α) (v : β k) (t : Impl α β) : Bool × Impl α β

Slower version of containsThenInsertIfNew which can be used in the absence of balance information but still assumes the preconditions of containsThenInsertIfNew, otherwise might panic.

Equations

• Std.DTreeMap.Internal.Impl.containsThenInsertIfNew! k v t = if Std.DTreeMap.Internal.Impl.contains k t = true then (true, t) else (false, Std.DTreeMap.Internal.Impl.insert! k v t)

@[inline]

def Std.DTreeMap.Internal.Impl.getThenInsertIfNew? {α : Type u} {β : α → Type v} [Ord α] [LawfulEqOrd α] (t : Impl α β) (k : α) (v : β k) (ht : t.Balanced) : Option (β k) × Impl α β

Implementation detail of the tree map

Equations

• t.getThenInsertIfNew? k v ht = match t.get? k with | none => (none, (Std.DTreeMap.Internal.Impl.insertIfNew k v t ht).impl) | some b => (some b, t)

@[inline]

def Std.DTreeMap.Internal.Impl.getThenInsertIfNew?! {α : Type u} {β : α → Type v} [Ord α] [LawfulEqOrd α] (t : Impl α β) (k : α) (v : β k) : Option (β k) × Impl α β

Slower version of getThenInsertIfNew? which can be used in the absence of balance information but still assumes the preconditions of getThenInsertIfNew?, otherwise might panic.

Equations

• t.getThenInsertIfNew?! k v = match t.get? k with | none => (none, Std.DTreeMap.Internal.Impl.insertIfNew! k v t) | some b => (some b, t)

def Std.DTreeMap.Internal.Impl.erase {α : Type u} {β : α → Type v} [Ord α] (k : α) (t : Impl α β) (h : t.Balanced) : SizedBalancedTree α β (t.size - 1) t.size

Removes the mapping with key k, if it exists.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.erase k Std.DTreeMap.Internal.Impl.leaf hr_1 = { impl := Std.DTreeMap.Internal.Impl.leaf, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }

def Std.DTreeMap.Internal.Impl.erase! {α : Type u} {β : α → Type v} [Ord α] (k : α) (t : Impl α β) : Impl α β

Slower version of erase which can be used in the absence of balance information but still assumes the preconditions of erase, otherwise might panic.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.erase! k Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.leaf

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Impl.IteratedErasureFrom {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) : Type (max 0 u v)

A tree map obtained by erasing elements from t, bundled with an inductive principle.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.DTreeMap.Internal.Impl.eraseMany {α : Type u} {β : α → Type v} [Ord α] {ρ : Type w} [ForIn Id ρ α] (t : Impl α β) (l : ρ) (h : t.Balanced) : t.IteratedErasureFrom

Iterate over l and erase all of its elements from t.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Impl.IteratedSlowErasureFrom {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) : Type (max 0 u v)

A tree map obtained by erasing elements from t, bundled with an inductive principle.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.DTreeMap.Internal.Impl.eraseMany! {α : Type u} {β : α → Type v} [Ord α] {ρ : Type w} [ForIn Id ρ α] (t : Impl α β) (l : ρ) : t.IteratedSlowErasureFrom

Slower version of eraseMany which can be used in absence of balance information but still assumes the preconditions of eraseMany, otherwise might panic.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Impl.IteratedInsertionInto {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) : Type (max 0 u v)

A tree map obtained by inserting elements into t, bundled with an inductive principle.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Impl.IteratedNewInsertionInto {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) : Type (max 0 u v)

A tree map obtained by inserting elements into t if they are new, bundled with an inductive principle.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.DTreeMap.Internal.Impl.insertMany {α : Type u} {β : α → Type v} [Ord α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] (t : Impl α β) (l : ρ) (h : t.Balanced) : t.IteratedInsertionInto

Iterate over l and insert all of its elements into t.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.DTreeMap.Internal.Impl.insertManyIfNew {α : Type u} {β : α → Type v} [Ord α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] (t : Impl α β) (l : ρ) (h : t.Balanced) : t.IteratedNewInsertionInto

Iterate over l and insert all of its elements into t if they are new.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Impl.IteratedSlowInsertionInto {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) : Type (max 0 u v)

A tree map obtained by inserting elements into t, bundled with an inductive principle.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Impl.IteratedSlowNewInsertionInto {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) : Type (max 0 u v)

A tree map obtained by inserting elements into t if they are new, bundled with an inductive principle.

Equations

• One or more equations did not get rendered due to their size.

def Std.DTreeMap.Internal.Impl.union {α : Type u} {β : α → Type v} [Ord α] (t₁ t₂ : Impl α β) (h₁ : t₁.Balanced) (h₂ : t₂.Balanced) : Impl α β

Computes the union of the given tree maps. If a key appears in both maps, the entry contained in the second argument will appear in the result.

This function always merges the smaller map into the larger map.

Equations

• t₁.union t₂ h₁ h₂ = if t₁.size ≤ t₂.size then (t₂.insertManyIfNew t₁ h₂).val else (t₁.insertMany t₂ h₁).val

@[inline]

def Std.DTreeMap.Internal.Impl.insertMany! {α : Type u} {β : α → Type v} [Ord α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] (t : Impl α β) (l : ρ) : t.IteratedSlowInsertionInto

Slower version of insertMany which can be used in absence of balance information but still assumes the preconditions of insertMany, otherwise might panic.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.DTreeMap.Internal.Impl.insertManyIfNew! {α : Type u} {β : α → Type v} [Ord α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] (t : Impl α β) (l : ρ) : t.IteratedSlowNewInsertionInto

Slower version of insertManyIfNew which can be used in absence of balance information but still assumes the preconditions of insertManyIfNew, otherwise might panic.

Equations

• One or more equations did not get rendered due to their size.

def Std.DTreeMap.Internal.Impl.union! {α : Type u} {β : α → Type v} [Ord α] (t₁ t₂ : Impl α β) : Impl α β

Slower version of union which can be used in absence of balance information but still assumes the preconditions of union, otherwise might panic.

Equations

• t₁.union! t₂ = if t₁.size ≤ t₂.size then (t₂.insertManyIfNew! t₁).val else (t₁.insertMany! t₂).val

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Impl.Const.IteratedInsertionInto {α : Type u} {β : Type v} [Ord α] (t : Impl α fun (x : α) => β) : Type (max 0 u v)

A tree map obtained by inserting elements into t, bundled with an inductive principle.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.DTreeMap.Internal.Impl.Const.insertMany {α : Type u} {β : Type v} [Ord α] {ρ : Type w} [ForIn Id ρ (α × β)] (t : Impl α fun (x : α) => β) (l : ρ) (h : t.Balanced) : IteratedInsertionInto t

Iterate over l and insert all of its elements into t.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Impl.Const.IteratedSlowInsertionInto {α : Type u} {β : Type v} [Ord α] (t : Impl α fun (x : α) => β) : Type (max 0 u v)

A tree map obtained by inserting elements into t, bundled with an inductive principle.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.DTreeMap.Internal.Impl.Const.insertMany! {α : Type u} {β : Type v} [Ord α] {ρ : Type w} [ForIn Id ρ (α × β)] (t : Impl α fun (x : α) => β) (l : ρ) : IteratedSlowInsertionInto t

Slower version of insertMany which can be used in absence of balance information but still assumes the preconditions of insertMany, otherwise might panic.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Impl.Const.IteratedUnitInsertionInto {α : Type u} [Ord α] (t : Impl α fun (x : α) => Unit) : Type u

A tree map obtained by inserting elements into t, bundled with an inductive principle.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit {α : Type u} [Ord α] {ρ : Type w} [ForIn Id ρ α] (t : Impl α fun (x : α) => Unit) (l : ρ) (h : t.Balanced) : IteratedUnitInsertionInto t

Iterate over l and insert all of its elements into t.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Impl.Const.IteratedSlowUnitInsertionInto {α : Type u} [Ord α] (t : Impl α fun (x : α) => Unit) : Type u

A tree map obtained by inserting elements into t, bundled with an inductive principle.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! {α : Type u} [Ord α] {ρ : Type w} [ForIn Id ρ α] (t : Impl α fun (x : α) => Unit) (l : ρ) : IteratedSlowUnitInsertionInto t

Slower version of insertManyIfNewUnit which can be used in absence of balance information but still assumes the preconditions of insertManyIfNewUnit, otherwise might panic.

Equations

• One or more equations did not get rendered due to their size.

structure Std.DTreeMap.Internal.Impl.BalancedTree (α : Type u) (β : α → Type v) : Type (max u v)

A balanced tree.

• impl : Impl α β

  The tree.

• balanced_impl : self.impl.Balanced

  The tree is balanced.

def Std.DTreeMap.Internal.Impl.SizedBalancedTree.toBalancedTree {α : Type u} {β : α → Type v} {lb ub : Nat} (t : SizedBalancedTree α β lb ub) : BalancedTree α β

Transforms an element of SizedBalancedTree into a BalancedTree.

Equations

• t.toBalancedTree = { impl := t.impl, balanced_impl := ⋯ }

@[inline]

def Std.DTreeMap.Internal.Impl.ofArray {α : Type u} {β : α → Type v} [Ord α] (a : Array ((a : α) × β a)) : Impl α β

Transforms an array of mappings into a tree map.

Equations

• Std.DTreeMap.Internal.Impl.ofArray a = (Std.DTreeMap.Internal.Impl.empty.insertMany a ⋯).val

@[inline]

def Std.DTreeMap.Internal.Impl.ofList {α : Type u} {β : α → Type v} [Ord α] (l : List ((a : α) × β a)) : Impl α β

Transforms a list of mappings into a tree map.

Equations

• Std.DTreeMap.Internal.Impl.ofList l = (Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯).val

@[inline]

def Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew? {α : Type u} {β : Type v} [Ord α] (t : Impl α fun (x : α) => β) (k : α) (v : β) (ht : t.Balanced) : Option β × Impl α fun (x : α) => β

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?! {α : Type u} {β : Type v} [Ord α] (t : Impl α fun (x : α) => β) (k : α) (v : β) : Option β × Impl α fun (x : α) => β

Slower version of getThenInsertIfNew? which can be used in the absence of balance information but still assumes the preconditions of getThenInsertIfNew?, otherwise might panic.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.DTreeMap.Internal.Impl.Const.ofArray {α : Type u} {β : Type v} [Ord α] (a : Array (α × β)) : Impl α fun (x : α) => β

Transforms a list of mappings into a tree map.

Equations

• Std.DTreeMap.Internal.Impl.Const.ofArray a = (Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty a ⋯).val

@[inline]

def Std.DTreeMap.Internal.Impl.Const.ofList {α : Type u} {β : Type v} [Ord α] (l : List (α × β)) : Impl α fun (x : α) => β

Transforms an array of mappings into a tree map.

Equations

• Std.DTreeMap.Internal.Impl.Const.ofList l = (Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯).val

@[inline]

def Std.DTreeMap.Internal.Impl.Const.unitOfArray {α : Type u} [Ord α] (a : Array α) : Impl α fun (x : α) => Unit

Transforms a list of mappings into a tree map.

Equations

• Std.DTreeMap.Internal.Impl.Const.unitOfArray a = (Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty a ⋯).val

@[inline]

def Std.DTreeMap.Internal.Impl.Const.unitOfList {α : Type u} [Ord α] (l : List α) : Impl α fun (x : α) => Unit

Transforms an array of mappings into a tree map.

Equations

• Std.DTreeMap.Internal.Impl.Const.unitOfList l = (Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty l ⋯).val

@[specialize #[]]

def Std.DTreeMap.Internal.Impl.filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [Ord α] (f : (a : α) → β a → Option (γ a)) (t : Impl α β) (hl : t.Balanced) : BalancedTree α γ

Returns the tree consisting of the mappings (k, (f k v).get) where (k, v) was a mapping in the original tree and (f k v).isSome.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.filterMap f Std.DTreeMap.Internal.Impl.leaf hr_1 = { impl := Std.DTreeMap.Internal.Impl.leaf, balanced_impl := ⋯ }

@[specialize #[]]

def Std.DTreeMap.Internal.Impl.filterMap! {α : Type u} {β : α → Type v} {γ : α → Type w} [Ord α] (f : (a : α) → β a → Option (γ a)) (t : Impl α β) : Impl α γ

Slower version of filterMap which can be used in the absence of balance information but still assumes the preconditions of filterMap, otherwise might panic.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.filterMap! f Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.leaf

@[specialize #[]]

def Std.DTreeMap.Internal.Impl.map {α : Type u} {β : α → Type v} {γ : α → Type w} [Ord α] (f : (a : α) → β a → γ a) (t : Impl α β) : Impl α γ

Returns the tree consisting of the mappings (k, f k v) where (k, v) was a mapping in the original tree.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.map f Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.leaf

@[specialize #[]]

def Std.DTreeMap.Internal.Impl.mapM {α : Type v} {β γ : α → Type v} {M : Type v → Type w} [Applicative M] (f : (a : α) → β a → M (γ a)) : Impl α β → M (Impl α γ)

Monadic version of map.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.mapM f Std.DTreeMap.Internal.Impl.leaf = pure Std.DTreeMap.Internal.Impl.leaf

@[specialize #[]]

def Std.DTreeMap.Internal.Impl.filter {α : Type u} {β : α → Type v} [Ord α] (f : (a : α) → β a → Bool) (t : Impl α β) (hl : t.Balanced) : BalancedTree α β

Returns the tree consisting of the mapping (k, v) where (k, v) was a mapping in the original tree and f k v = true.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.filter f Std.DTreeMap.Internal.Impl.leaf hr_1 = { impl := Std.DTreeMap.Internal.Impl.leaf, balanced_impl := ⋯ }

@[specialize #[]]

def Std.DTreeMap.Internal.Impl.filter! {α : Type u} {β : α → Type v} [Ord α] (f : (a : α) → β a → Bool) (t : Impl α β) : Impl α β

Slower version of filter which can be used in the absence of balance information but still assumes the preconditions of filter, otherwise might panic.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.filter! f Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.leaf

@[specialize #[]]

def Std.DTreeMap.Internal.Impl.alter {α : Type u} {β : α → Type v} [Ord α] [LawfulEqOrd α] (k : α) (f : Option (β k) → Option (β k)) (t : Impl α β) (hl : t.Balanced) : SizedBalancedTree α β (t.size - 1) (t.size + 1)

Changes the mapping of the key k by applying the function f to the current mapped value (if any). This function can be used to insert a new mapping, modify an existing one or delete it. This version of the function requires LawfulEqOrd α. There is an alternative non-dependent version called Const.alter.

Equations

• One or more equations did not get rendered due to their size.

@[specialize #[]]

def Std.DTreeMap.Internal.Impl.alter! {α : Type u} {β : α → Type v} [Ord α] [LawfulEqOrd α] (k : α) (f : Option (β k) → Option (β k)) (t : Impl α β) : Impl α β

Slower version of modify which can be used in the absence of balance information but still assumes the preconditions of modify, otherwise might panic.

Equations

• One or more equations did not get rendered due to their size.

@[specialize #[]]

def Std.DTreeMap.Internal.Impl.modify {α : Type u} {β : α → Type v} [Ord α] [LawfulEqOrd α] (k : α) (f : β k → β k) (t : Impl α β) : Impl α β

Internal implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.modify k f Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.leaf

theorem Std.DTreeMap.Internal.Impl.aux_size_modify {α : Type u} {β : α → Type v} [Ord α] [LawfulEqOrd α] {k : α} {f : β k → β k} {t : Impl α β} : (modify k f t).size = t.size

theorem Std.DTreeMap.Internal.Impl.balanced_modify {α : Type u} {β : α → Type v} [Ord α] [LawfulEqOrd α] {k : α} {f : β k → β k} {t : Impl α β} (ht : t.Balanced) : (modify k f t).Balanced

@[inline]

def Std.DTreeMap.Internal.Impl.mergeWith {α : Type u} {β : α → Type v} [Ord α] [LawfulEqOrd α] (mergeFn : (a : α) → β a → β a → β a) (t₁ t₂ : Impl α β) (ht₁ : t₁.Balanced) : BalancedTree α β

Returns a map that contains all mappings of t₁ and t₂. In case that both maps contain the same key k with respect to cmp, the provided function is used to determine the new value from the respective values in t₁ and t₂.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.DTreeMap.Internal.Impl.mergeWith! {α : Type u} {β : α → Type v} [Ord α] [LawfulEqOrd α] (mergeFn : (a : α) → β a → β a → β a) (t₁ t₂ : Impl α β) : Impl α β

Returns a map that contains all mappings of t₁ and t₂. In case that both maps contain the same key k with respect to cmp, the provided function is used to determine the new value from the respective values in t₁ and t₂.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Std.DTreeMap.Internal.Impl.Const.instCoeTypeForall = { coe := fun (γ : Type ?u.10) (x : α) => γ }

@[specialize #[]]

def Std.DTreeMap.Internal.Impl.Const.alter {α : Type u} {β : Type v} [Ord α] (k : α) (f : Option β → Option β) (t : Impl α fun (x : α) => β) (hl : t.Balanced) : SizedBalancedTree α (fun (x : α) => β) (t.size - 1) (t.size + 1)

Changes the mapping of the key k by applying the function f to the current mapped value (if any). This function can be used to insert a new mapping, modify an existing one or delete it. This version of the function requires LawfulEqOrd α. There is an alternative non-dependent version called Const.alter.

Equations

• One or more equations did not get rendered due to their size.

@[specialize #[]]

def Std.DTreeMap.Internal.Impl.Const.alter! {α : Type u} {β : Type v} [Ord α] (k : α) (f : Option β → Option β) (t : Impl α fun (x : α) => β) : Impl α fun (x : α) => β

Slower version of modify which can be used in the absence of balance information but still assumes the preconditions of modify, otherwise might panic.

Equations

• One or more equations did not get rendered due to their size.

@[specialize #[]]

def Std.DTreeMap.Internal.Impl.Const.modify {α : Type u} {β : Type v} [Ord α] (k : α) (f : β → β) (t : Impl α fun (x : α) => β) : Impl α fun (x : α) => β

Internal implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.modify k f Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.leaf

theorem Std.DTreeMap.Internal.Impl.Const.aux_size_modify {α : Type u} {β : Type v} [Ord α] {k : α} {f : β → β} {t : Impl α fun (x : α) => β} : (modify k f t).size = t.size

theorem Std.DTreeMap.Internal.Impl.Const.balanced_modify {α : Type u} {β : Type v} [Ord α] {k : α} {f : β → β} {t : Impl α fun (x : α) => β} (ht : t.Balanced) : (modify k f t).Balanced

@[inline]

def Std.DTreeMap.Internal.Impl.Const.mergeWith {α : Type u} {β : Type v} [Ord α] (mergeFn : α → β → β → β) (t₁ t₂ : Impl α fun (x : α) => β) (ht₁ : t₁.Balanced) : BalancedTree α fun (x : α) => β

Returns a map that contains all mappings of t₁ and t₂. In case that both maps contain the same key k with respect to cmp, the provided function is used to determine the new value from the respective values in t₁ and t₂.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.DTreeMap.Internal.Impl.Const.mergeWith! {α : Type u} {β : Type v} [Ord α] (mergeFn : α → β → β → β) (t₁ t₂ : Impl α fun (x : α) => β) : Impl α fun (x : α) => β

Returns a map that contains all mappings of t₁ and t₂. In case that both maps contain the same key k with respect to cmp, the provided function is used to determine the new value from the respective values in t₁ and t₂.

Equations

• One or more equations did not get rendered due to their size.