Documentation

Std.Data.DTreeMap.Internal.Operations

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 #

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

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

A balanced tree of the given size.

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

source
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
source
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
source
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
source
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

glue #

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

insertMin and insertMax #

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

Modification operations #

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

source
@[inline]
def Std.DTreeMap.Internal.Impl.empty {α : Type u} {β : α → Type v} :
Impl α β

An empty tree.

Equations
source
theorem Std.DTreeMap.Internal.Impl.balanced_empty {α : Type u} {β : α → Type v} :
empty.Balanced
source
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.
source
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
source
@[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.
source
def Std.DTreeMap.Internal.Impl.containsThenInsert.size {α : Type u} {β : α → Type v} :
Impl α β → Nat
Equations
source
@[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.
source
def Std.DTreeMap.Internal.Impl.containsThenInsert!.size {α : Type u} {β : α → Type v} :
Impl α β → Nat
Equations
source
@[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.
source
@[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
source
@[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.
source
@[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
source
@[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
source
@[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
source
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
source
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
source
@[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.
source
@[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.
source
@[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.
source
@[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.
source
@[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.
source
@[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.
source
@[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.
source
@[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.
source
@[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.
source
@[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.
source
@[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.
source
@[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.
source
@[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.
source
@[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.
source
@[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.
source
@[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.
source
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.

source
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
source
@[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
source
@[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
source
@[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.
source
@[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.
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[specialize #[]]
def Std.DTreeMap.Internal.Impl.mapM {α : Type v} {β γ : α → Type v} {M : Type v → Type v} [Applicative M] (f : (a : α) → β a → M (γ a)) :
Impl α β → M (Impl α γ)

Monadic version of map.

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