Binary tree #
Provides binary tree storage for values of any type, with O(lg n) retrieval.
See also Lean.Data.RBTree
for red-black trees - this version allows more operations
to be defined and is better suited for in-kernel computation.
We also specialize for Tree Unit
, which is a binary tree without any
additional data. We provide the notation a △ b
for making a Tree Unit
with children
a
and b
.
References #
https://leanprover-community.github.io/archive/stream/113488-general/topic/tactic.20question.html
Do an action for every node of the tree.
Actions are taken in node -> left subtree -> right subtree recursive order.
This function is the traverse
function for the Traversable Tree
instance.
Equations
Instances For
The number of internal nodes (i.e. not including leaves) of a binary tree
Equations
Instances For
The number of leaves of a binary tree
Equations
Instances For
The height - length of the longest path from the root - of a binary tree