Documentation

Mathlib.Data.Tree.Basic

Binary tree #

Provides binary tree storage for values of any type, with O(lg n) retrieval. See also Lean.Data.RBTree for red-black trees - this version allows more operations to be defined and is better suited for in-kernel computation.

We also specialize for Tree Unit, which is a binary tree without any additional data. We provide the notation a △ b for making a Tree Unit with children a and b.

References #

https://leanprover-community.github.io/archive/stream/113488-general/topic/tactic.20question.html

inductive Tree (α : Type u) :

A binary tree with values stored in non-leaf nodes.

Instances For
    instance instDecidableEqTree {α✝ : Type u_1} [DecidableEq α✝] :
    Equations
      instance instReprTree {α✝ : Type u_1} [Repr α✝] :
      Repr (Tree α✝)
      Equations
        instance Tree.instInhabited {α : Type u} :
        Equations
          def Tree.traverse {m : Type u_1 → Type u_2} [Applicative m] {α : Type u_3} {β : Type u_1} (f : αm β) :
          Tree αm (Tree β)

          Do an action for every node of the tree. Actions are taken in node -> left subtree -> right subtree recursive order. This function is the traverse function for the Traversable Tree instance.

          Equations
            Instances For
              def Tree.map {α : Type u} {β : Type u_1} (f : αβ) :
              Tree αTree β

              Apply a function to each value in the tree. This is the map function for the Tree functor.

              Equations
                Instances For
                  theorem Tree.id_map {α : Type u} (t : Tree α) :
                  map id t = t
                  theorem Tree.comp_map {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβ) (g : βγ) (t : Tree α) :
                  map (g f) t = map g (map f t)
                  theorem Tree.traverse_pure {α : Type u} (t : Tree α) {m : Type u → Type u_1} [Applicative m] [LawfulApplicative m] :
                  def Tree.numNodes {α : Type u} :
                  Tree α

                  The number of internal nodes (i.e. not including leaves) of a binary tree

                  Equations
                    Instances For
                      def Tree.numLeaves {α : Type u} :
                      Tree α

                      The number of leaves of a binary tree

                      Equations
                        Instances For
                          def Tree.height {α : Type u} :
                          Tree α

                          The height - length of the longest path from the root - of a binary tree

                          Equations
                            Instances For
                              theorem Tree.numLeaves_pos {α : Type u} (x : Tree α) :
                              theorem Tree.height_le_numNodes {α : Type u} (x : Tree α) :
                              def Tree.left {α : Type u} :
                              Tree αTree α

                              The left child of the tree, or nil if the tree is nil

                              Equations
                                Instances For
                                  def Tree.right {α : Type u} :
                                  Tree αTree α

                                  The right child of the tree, or nil if the tree is nil

                                  Equations
                                    Instances For

                                      A node with Unit data

                                      Equations
                                        Instances For
                                          def Tree.unitRecOn {motive : Tree UnitSort u_1} (t : Tree Unit) (base : motive nil) (ind : (x y : Tree Unit) → motive xmotive ymotive (node () x y)) :
                                          motive t

                                          Induction principle for Tree Units

                                          Equations
                                            Instances For