From 9739358158e3c69140d5ac5ade63ba9169405e0a Mon Sep 17 00:00:00 2001 From: Jannis Limperg Date: Tue, 1 Oct 2024 14:39:38 +0200 Subject: [PATCH] Builder.Apply: suggest alias when warning about apply rule for Iff theorem (#163) --- Aesop/Builder/Apply.lean | 2 +- AesopTest/WarnApplyIff.lean | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) 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