Low-level implementation of the size-bounded tree #
This file contains the basic definition implementing the functionality of the size-bounded trees.
@[inline]
The "delta" parameter of the size-bounded tree. Controls how imbalanced the tree can be.
Equations
Instances For
@[inline]
The "ratio" parameter of the size-bounded tree. Controls how aggressive the rebalancing operations are.
Equations
Instances For
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
).
toListModel
#
toListModel
is defined here because it is required to define the Ordered
predicate.
@[simp]
@[simp]
theorem
Std.DTreeMap.Internal.Impl.toListModel_inner
{α : Type u}
{β : α → Type v}
{sz : Nat}
{k : α}
{v : β k}
{l r : Impl α β}
: