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

tree.of_rbnode

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

tree.index_of

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.

tree.get

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 child
bit1 - go to right child
one - retrieve from here

tree.get_or_else

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