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.

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
    source
    def Std.DTreeMap.Internal.instInhabitedImpl.default {a✝ : Type u_1} {a✝¹ : a✝ → Type u_2} :
    Impl a✝ a✝¹
    Equations
    Instances For
      source
      @[inline]
      def Std.DTreeMap.Internal.delta :
      Nat

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

      Equations
      Instances For
        source
        @[inline]
        def Std.DTreeMap.Internal.ratio :
        Nat

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

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

          The size information stored in the tree.

          Equations
          Instances For
            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
            Instances For
              source
              @[simp]
              theorem Std.DTreeMap.Internal.Impl.toListModel_leaf {α : Type u} {β : α → Type v} :
              leaf.toListModel = []
              source
              @[simp]
              theorem Std.DTreeMap.Internal.Impl.toListModel_inner {α : Type u} {β : α → Type v} {sz : Nat} {k : α} {v : β k} {l r : Impl α β} :
              (inner sz k v l r).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel
              source
              def Std.DTreeMap.Internal.Impl.treeSize {α : Type u} {β : α → Type v} :
              Impl α β → Nat

              Computes the size of the tree. Used for verification of iterators.

              Equations
              Instances For