Binary tree #
Provides binary tree storage for values of any type, with O(lg n) retrieval.
Lean.Data.RBTree for red-black trees - this version allows more operations
to be defined and is better suited for in-kernel computation.
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.
Retrieves an element uniquely determined by a
PosNum from the tree,
taking the following path to get to the element: