Commit 2025-09-10 06:51 9ec894fd

View on Github →

feat: changes to tactic analysis linter (#29460) Some code cleanup and more features for the grindReplacementWith passes.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Lean/Elab/Tactic/Meta.lean

added def Lean.Elab.runTactic'

Modified Mathlib/Tactic/TacticAnalysis.lean

Modified Mathlib/Tactic/TacticAnalysis/Declarations.lean

modified def grindReplacementWith

modified def omegaToGrind