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

source

inductive tree :

Type u → Type u

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

source

@[instance]

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

has_reflect (tree α)

source

@[instance]

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

decidable_eq (tree α)

source

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

tree α → string

Equations

(tree.node a t1 t2).repr = "tree.node " ++ has_repr.repr a ++ " (" ++ t1.repr ++ ") (" ++ t2.repr ++ ")"
tree.nil.repr = "nil"

source

@[instance]

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

has_repr (tree α)

Equations

tree.has_repr = {repr := tree.repr _inst_1}

source

@[instance]

def tree.inhabited {α : Type u} :

inhabited (tree α)

Equations

tree.inhabited = {default := tree.nil α}

source

def tree.of_rbnode {α : Type u} :

rbnode α → tree α

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

Equations

tree.of_rbnode (l.black_node a r) = tree.node a (tree.of_rbnode l) (tree.of_rbnode r)
tree.of_rbnode (l.red_node a r) = tree.node a (tree.of_rbnode l) (tree.of_rbnode r)
tree.of_rbnode rbnode.leaf = tree.nil

source

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