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

def Tree.ofRBNode {α : Type u} : Batteries.RBNode α → Tree α

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

Equations

• Tree.ofRBNode Batteries.RBNode.nil = Tree.nil
• Tree.ofRBNode (Batteries.RBNode.node _color l key r) = Tree.node key (Tree.ofRBNode l) (Tree.ofRBNode r)