diff --git a/Aesop/Builder/Apply.lean b/Aesop/Builder/Apply.lean index 9579f17..b6f2b7b 100644 --- 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 index 0e1bf32..972b57f 100644 --- 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