.

Author: kim-em

Mathlib/Tactic/TacticAnalysis/Declarations.lean

@@ -8,6 +8,7 @@ import Mathlib.Tactic.ExtractGoal
 import Mathlib.Tactic.MinImports
 import Lean.Elab.Tactic.Meta
 import Lean.Elab.Command
+import Aesop
 
 /-!
 # Tactic linters
@@ -322,6 +323,24 @@ def tryAtEachStepAesop := tryAtEachStep
   fun _ _ => return ⟨TSyntax.raw <|
     mkNode `Aesop.Frontend.Parser.aesopTactic #[mkAtom "aesop", mkNullNode]⟩
 
+/-- Run `simp_all` at every step in proofs, reporting where it succeeds. -/
+register_option linter.tacticAnalysis.tryAtEachStepSimpAll : Bool := {
+  defValue := false
+}
+
+@[tacticAnalysis linter.tacticAnalysis.tryAtEachStepSimpAll,
+   inherit_doc linter.tacticAnalysis.tryAtEachStepSimpAll]
+def tryAtEachStepSimpAll := tryAtEachStep (fun _ => `(tactic| simp_all))
+
+/-- Run `aesop` at every step in proofs, reporting where it succeeds. -/
+register_option linter.tacticAnalysis.tryAtEachStepAesop : Bool := {
+  defValue := false
+}
+
+@[tacticAnalysis linter.tacticAnalysis.tryAtEachStepAesop,
+   inherit_doc linter.tacticAnalysis.tryAtEachStepAesop]
+def tryAtEachStepAesop := tryAtEachStep (fun _ => `(tactic| aesop))
+
 /-- Run `grind +premises` at every step in proofs, reporting where it succeeds. -/
 register_option linter.tacticAnalysis.tryAtEachStepGrindPremises : Bool := {
   defValue := false