Commit 2025-10-31 08:48 184ad813

View on Github →

feat: tryAtEachStep linters run on a fraction of goals (#31039) This PR allows us to run the tryAtEachStep linters on a deterministic fraction of all Mathlib goals, to enable faster benchmarks.

Estimated changes

Modified Mathlib/Tactic/TacticAnalysis/Declarations.lean

added def Mathlib.TacticAnalysis.introMerge

added def Mathlib.TacticAnalysis.mergeWithGrind

added def Mathlib.TacticAnalysis.rwMerge

added def Mathlib.TacticAnalysis.terminalToGrind

added def Mathlib.TacticAnalysis.tryAtEachStep

deleted def introMerge

deleted def mergeWithGrind

deleted def rwMerge

deleted def terminalToGrind

deleted def tryAtEachStep

modified def tryAtEachStepGrind

modified def tryAtEachStepGrindPremises

modified def tryAtEachStepSimpAll

Modified MathlibTest/tryAtEachStep.lean

added theorem bar