Binary tree and RBMaps #
In this file we define Tree.ofRBNode
.
This definition was moved from the main file to avoid a dependency on RBMap
.
TODO #
Implement a Traversable
instance for Tree
.
References #
https://leanprover-community.github.io/archive/stream/113488-general/topic/tactic.20question.html