mathlib documentation

data.tree

Binary tree

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

References

https://leanprover-community.github.io/archive/113488general/62193tacticquestion.html

@[instance]
def tree.decidable_eq (α : Type u) [a : decidable_eq α] :

@[instance]
meta def tree.has_reflect (α : Type) [a : has_reflect α] [a_1 : reflected α] :

inductive tree  :
Type uType u
  • nil : Π (α : Type u), tree α
  • node : Π (α : Type u), α → tree αtree αtree α

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

def tree.repr {α : Type u} [has_repr α] :
tree αstring

Construct a string representation of a tree. Provides a has_repr instance.

Equations
@[instance]
def tree.has_repr {α : Type u} [has_repr α] :

Equations
@[instance]
def tree.inhabited {α : Type u} :

Equations
def tree.of_rbnode {α : Type u} :
rbnode αtree α

Makes a tree α out of a red-black tree.

Equations
def tree.index_of {α : Type u} (lt : α → α → Prop) [decidable_rel lt] :
α → tree αoption pos_num

Finds the index of an element in the tree assuming the tree has been constructed according to the provided decidable order on its elements. If it hasn't, the result will be incorrect. If it has, but the element is not in the tree, returns none.

Equations
def tree.get {α : Type u} :
pos_numtree αoption α

Retrieves an element uniquely determined by a pos_num from the tree, taking the following path to get to the element:

Equations
def tree.get_or_else {α : Type u} :
pos_numtree αα → α

Retrieves an element from the tree, or the provided default value if the index is invalid. See tree.get.

Equations
def tree.map {α : Type u} {β : Type u_1} :
(α → β)tree αtree β

Apply a function to each value in the tree. This is the map function for the tree functor. TODO: implement traversable tree.

Equations