Commit 2024-06-08 18:34 c995db1f

View on Github →

chore(Data/Tree): split file (#13629) Move 3 definitions that depend on Num to a new file.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/Enumerative/Catalan.lean

Renamed Mathlib/Data/Tree.lean to Mathlib/Data/Tree/Basic.lean

deleted def Tree.get

deleted def Tree.getOrElse

deleted def Tree.indexOf

Created Mathlib/Data/Tree/Get.lean

added def Tree.get

added def Tree.getOrElse

added def Tree.indexOf

Modified Mathlib/Tactic/CancelDenoms/Core.lean