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/stream/113488-general/topic/tactic.20question.html
A binary tree with values stored in non-leaf nodes.
Instances for tree
- tree.has_sizeof_inst
- tree.has_reflect
- tree.has_repr
- tree.inhabited
- slim_check.tree.functor
- slim_check.sampleable_tree
Equations
- tree.has_repr = {repr := tree.repr _inst_1}
Equations
- tree.inhabited = {default := tree.nil α}
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
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
- tree.index_of lt x (tree.node a t₁ t₂) = tree.index_of._match_1 (tree.index_of lt x t₁) (tree.index_of lt x t₂) (cmp_using lt x a)
- tree.index_of lt x tree.nil = option.none
- tree.index_of._match_1 _f_1 _f_2 ordering.gt = pos_num.bit1 <$> _f_2
- tree.index_of._match_1 _f_1 _f_2 ordering.eq = option.some pos_num.one
- tree.index_of._match_1 _f_1 _f_2 ordering.lt = pos_num.bit0 <$> _f_1
Retrieves an element uniquely determined by a pos_num
from the tree,
taking the following path to get to the element:
bit0
- go to left childbit1
- go to right childpos_num.one
- retrieve from here
Equations
- tree.get n.bit0 (tree.node a t₁ t₂) = tree.get n t₁
- tree.get ᾰ.bit0 tree.nil = option.none
- tree.get n.bit1 (tree.node a t₁ t₂) = tree.get n t₂
- tree.get ᾰ.bit1 tree.nil = option.none
- tree.get pos_num.one (tree.node a t₁ t₂) = option.some a
- tree.get pos_num.one tree.nil = option.none
Retrieves an element from the tree, or the provided default value
if the index is invalid. See tree.get
.
Equations
- tree.get_or_else n t v = (tree.get n t).get_or_else v
Apply a function to each value in the tree. This is the map
function for the tree
functor.
TODO: implement traversable tree
.