Provides binary tree storage for values of any type, with O(lg n) retrieval.
data.rbtree for red-black trees - this version allows more operations
to be defined and is better suited for in-kernel computation.
tree α out of a red-black tree.
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.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 = 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 = 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: