Def Tree.ofRBNode

Modification history

2024-10-15 10:13

Mathlib/Data/Tree/Basic.lean

chore: split off `RBMap` dependency from `Mathlib.Data.Tree` (#17764) …

Modified Tree.ofRBNode View on Github →

2023-03-12 12:39

Mathlib/Data/Tree.lean

feat: Port Data.Tree (#2587)

Added Tree.ofRBNode View on Github →