Commit 2025-01-01 22:55 ec10d9ba
View on Github →chore: split Lean/Meta/RefinedDiscrTree
(#20381)
This split is intended to roughly match #11968, in order to reduce the diff there. I will take ownership of fixing any resulting merge conflicts.
The declarations have been copied unchanged between files, with the exception of a single removed private
on DTExpr.eqv
that prevented this split. Refactors are left to #11968.
The namespace of all the declarations has changed from Mathlib.Meta.FunProp.RefinedDiscrTree
to Lean.Meta.RefinedDiscrTree
, to match the filename.