Builder.Apply: suggest alias when warning about apply rule for Iff th…

…eorem (#163)
leanprover-community · Oct 1, 2024 · 9739358 · 9739358
1 parent 28fa805
commit 9739358
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/Aesop/Builder/Apply.lean b/Aesop/Builder/Apply.lean
@@ -34,7 +34,7 @@ def checkNoIff (type : Expr) : MetaM Unit := do
   if aesop.warn.applyIff.get (← getOptions) then
     forallTelescope type λ _ conclusion => do
       if ← testHelper conclusion λ e => return e.isAppOf' ``Iff then
-        logWarning m!"Apply builder was used for a theorem with conclusion A ↔ B. You probably want to use the simp builder.\nUse `set_option aesop.warn.applyIff false` to disable this warning."
+        logWarning m!"Apply builder was used for a theorem with conclusion A ↔ B.\nYou probably want to use the simp builder or create an alias that applies the theorem in one direction.\nUse `set_option aesop.warn.applyIff false` to disable this warning."
 
 def applyCore (t : ElabRuleTerm) (pat? : Option RulePattern)
     (imode? : Option IndexingMode) (md indexMd : TransparencyMode)

diff --git a/AesopTest/WarnApplyIff.lean b/AesopTest/WarnApplyIff.lean
@@ -9,7 +9,8 @@ import Aesop
 set_option aesop.check.all true
 
 /--
-warning: Apply builder was used for a theorem with conclusion A ↔ B. You probably want to use the simp builder.
+warning: Apply builder was used for a theorem with conclusion A ↔ B.
+You probably want to use the simp builder or create an alias that applies the theorem in one direction.
 Use `set_option aesop.warn.applyIff false` to disable this warning.
 -/
 #guard_msgs in