Commit 2025-09-16 13:27 d19d8dee

View on Github →

feat: generalize terminal tactic analysis (#29694) This PR generalizes the existing tactic analysis tools for identifying successes or failures of replacing terminal tactics with grind, to the case of replacing one terminal tactic by another.

Estimated changes

Modified Mathlib/Computability/AkraBazzi/AkraBazzi.lean

Modified Mathlib/Tactic/TacticAnalysis.lean

Modified Mathlib/Tactic/TacticAnalysis/Declarations.lean

added def Mathlib.TacticAnalysis.grindReplacementWith

added def Mathlib.TacticAnalysis.terminalReplacement

deleted def grindReplacementWith

deleted def linarithToGrind

added def linarithToGrindRegressions

added def omegaToCutsat

added def omegaToCutsatRegressions

deleted def omegaToGrind

deleted def ringToGrind

added def ringToGrindRegressions

Modified MathlibTest/TacticAnalysis.lean