Def Tree.ofRBNode

Modification history

2025-10-31 08:47

Mathlib/Data/Tree/RBMap.lean

chore: remove declarations deprecated before 2025-04-21 (#30759) …

Deleted Tree.ofRBNode View on Github →

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 →