Documentation

Std.Data.DTreeMap.Internal.Def

Low-level implementation of the size-bounded tree #

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

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
    instance Std.DTreeMap.Internal.instInhabitedImpl {a✝ : Type u_1} {a✝¹ : a✝Type u_2} :
    Inhabited (Impl a✝ a✝¹)
    Equations
      @[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).

              @[inline]
              def Std.DTreeMap.Internal.Impl.size {α : Type u} {β : αType v} :
              Impl α βNat

              The size information stored in the tree.

              Equations
                Instances For
                  theorem Std.DTreeMap.Internal.Impl.size_leaf {α : Type u} {β : αType v} :
                  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.

                  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
                    Instances For
                      @[simp]
                      theorem Std.DTreeMap.Internal.Impl.toListModel_inner {α : Type u} {β : αType v} {sz : Nat} {k : α} {v : β k} {l r : Impl α β} :