Commit 2026-09-04 14:00 753d4cb3

View on Github →

chore(Tactic/Clean): deprecate clean% (#43413) The clean tactic an clean% term elaborators are very old and are not used or useful anymore. So, we deprecate them.

Estimated changes

Modified Mathlib/Tactic/Clean.lean

Deleted MathlibTest/Tactic/Clean.lean

deleted theorem Tests.withClean

deleted theorem Tests.withoutClean

deleted def Tests.x'

deleted def Tests.x