Low-level implementation of the size-bounded tree #

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

source

inductive Std.DTreeMap.Internal.Impl (α : Type u) (β : α → Type v) :

Type (max u v)

(Implementation detail) The actual inductive type for the size-balanced tree data structure.

inner {α : Type u} {β : α → Type v} (size : Nat) (k : α) (v : β k) (l r : Impl α β) : Impl α β
(Implementation detail)
leaf {α : Type u} {β : α → Type v} : Impl α β
(Implementation detail)

Instances For

source

instance Std.DTreeMap.Internal.instInhabitedImpl {a✝ : Type u_1} {a✝¹ : a✝ → Type u_2} :

Inhabited (Impl a✝ a✝¹)

Equations

Std.DTreeMap.Internal.instInhabitedImpl = { default := Std.DTreeMap.Internal.Impl.leaf }

source

@[inline]

def Std.DTreeMap.Internal.delta :

Nat

The "delta" parameter of the size-bounded tree. Controls how imbalanced the tree can be.

Equations

Std.DTreeMap.Internal.delta = 3

source

@[inline]

def Std.DTreeMap.Internal.ratio :

Nat

The "ratio" parameter of the size-bounded tree. Controls how aggressive the rebalancing operations are.

Equations

Std.DTreeMap.Internal.ratio = 2

`size` #

In contrast to other functions, size is defined here because it is required to define the Balanced predicate (see Std.Data.DTreeMap.Internal.Balanced).

source

@[inline]

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

Impl α β → Nat

The size information stored in the tree.

Equations

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

source

theorem Std.DTreeMap.Internal.Impl.size_leaf {α : Type u} {β : α → Type v} :

leaf.size = 0

source

theorem Std.DTreeMap.Internal.Impl.size_inner {α : Type u} {β : α → Type v} {sz : Nat} {k : α} {v : β k} {l r : Impl α β} :

(inner sz k v l r).size = sz

`toListModel` #

toListModel is defined here because it is required to define the Ordered predicate.

source

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

Impl α β → List ((a : α) × β a)

Flattens a tree into a list of key-value pairs. This function is defined for verification purposes and should not be executed because it is very inefficient.

Equations