fix simpComm linter

leanprover-community · Nov 18, 2024 · 899ed8a · 899ed8a
1 parent 537fdfa
commit 899ed8a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Batteries/Tactic/Lint/Simp.lean b/Batteries/Tactic/Lint/Simp.lean
@@ -228,7 +228,7 @@ private def Expr.eqOrIff? : Expr → Option (Expr × Expr)
   noErrorsFound := "No commutativity lemma is marked simp."
   errorsFound := "COMMUTATIVITY LEMMA IS SIMP.
 Some commutativity lemmas are simp lemmas:"
-  test := fun declName => withReducible do
+  test := fun declName => withSimpGlobalConfig do withReducible do
     unless ← isSimpTheorem declName do return none
     let ty := (← getConstInfo declName).type
     forallTelescopeReducing ty fun _ ty' => do