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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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

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

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.

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.

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.

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

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

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

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

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

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

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

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

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

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

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.

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.

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

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

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

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

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Impl.IteratedEntryErasureFrom {α : 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.

@[inline]

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

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

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Impl.IteratedSlowEntryErasureFrom {α : 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.

@[inline]

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

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

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

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

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

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

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

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

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.

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

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

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.

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

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

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

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

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

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

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

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

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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[inline]

def Std.DTreeMap.Internal.Impl.interSmallerFn {α : Type u} {β : α → Type v} [Ord α] (m : Impl α β) (sofar : { t : Impl α β // t.Balanced }) (k : α) : { res : Impl α β // res.Balanced }

Internal implementation detail of the tree map

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

Internal implementation detail of the tree map

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

Internal implementation detail of the hash map

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

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

def Std.DTreeMap.Internal.Impl.beq {α : Type u} {β : α → Type v} [Ord α] [LawfulEqOrd α] [(k : α) → BEq (β k)] (t₁ t₂ : Impl α β) : Bool

Internal implementation detail of the tree map

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

Computes the difference of the given tree maps. This function always iterates through the smaller map.

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

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

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

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

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

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

theorem Std.DTreeMap.Internal.Impl.balanced_inter {α : Type u} {β : α → Type v} [Ord α] {t₁ t₂ : Impl α β} (ht : t₁.Balanced) : (t₁.inter t₂ ht).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₂.

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

def Std.DTreeMap.Internal.Impl.Const.beq {α : Type u} {β : Type v} [Ord α] [BEq β] (t₁ t₂ : Impl α fun (x : α) => β) : Bool

Internal implementation detail of the hash map

@[implicit_reducible]

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

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

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

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

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₂.

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