From 04adc21251924205bf31e0176f04107a9db3a0ea Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Mon, 23 Dec 2024 13:47:10 +0100
Subject: [PATCH] improve error message

---
 Mathlib/Tactic/ToAdditive/Frontend.lean |  4 +++-
 MathlibTest/toAdditive.lean             | 15 ++++++++++++---
 2 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Tactic/ToAdditive/Frontend.lean b/Mathlib/Tactic/ToAdditive/Frontend.lean
index 7d4f031891763..6e1942fba38c6 100644
--- a/Mathlib/Tactic/ToAdditive/Frontend.lean
+++ b/Mathlib/Tactic/ToAdditive/Frontend.lean
@@ -1183,9 +1183,11 @@ partial def applyAttributes (stx : Syntax) (rawAttrs : Array Syntax) (thisAttr s
   if linter.existingAttributeWarning.get (← getOptions) then
     let appliedAttrs ← getAllSimpAttrs src
     if appliedAttrs.size > 0 then
+      let appliedAttrs := ", ".intercalate (appliedAttrs.toList.map toString)
+      -- Note: we're not bothering to print the correct attribute arguments.
       Linter.logLintIf linter.existingAttributeWarning stx m!"\
         The source declaration {src} was given the simp-attribute(s) {appliedAttrs} before \
-        calling @[{thisAttr}]. The preferred method is to use \
+        calling @[{thisAttr}]. The preferred method is to use something like \
         `@[{thisAttr} (attr := {appliedAttrs})]` to apply the attribute to both \
         {src} and the target declaration {tgt}."
     warnAttr stx Lean.Elab.Tactic.Ext.extExtension
diff --git a/MathlibTest/toAdditive.lean b/MathlibTest/toAdditive.lean
index 91b979c8d8095..a1f60be919017 100644
--- a/MathlibTest/toAdditive.lean
+++ b/MathlibTest/toAdditive.lean
@@ -1,5 +1,6 @@
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Lean.Exception
+import Mathlib.Tactic.ReduceModChar.Ext
 import Qq.MetaM
 open Qq Lean Meta Elab Command ToAdditive
 
@@ -109,9 +110,6 @@ lemma foo15 {α β : Type u} [my_has_pow α β] (x : α) (y : β) : foo14 x y =
 @[to_additive (reorder := 1 2, 4 5) bar16]
 lemma foo16 {α β : Type u} [my_has_pow α β] (x : α) (y : β) : foo14 x y = (x ^ y) ^ y := foo15 x y
 
-initialize testExt : SimpExtension ←
-  registerSimpAttr `simp_test "test"
-
 @[to_additive bar17]
 def foo17 [Group α] (x : α) : α := x * 1
 
@@ -424,3 +422,14 @@ run_cmd do
   unless findTranslation? (← getEnv) `localize.r == some `add_localize.r do throwError "1"
   unless findTranslation? (← getEnv) `localize   == some `add_localize   do throwError "2"
   unless findTranslation? (← getEnv) `localize.s == some `add_localize.s do throwError "3"
+
+/--
+warning: The source declaration one_eq_one was given the simp-attribute(s) reduce_mod_char, simp before calling @[to_additive]. The preferred method is to use something like `@[to_additive (attr := reduce_mod_char, simp)]` to apply the attribute to both one_eq_one and the target declaration zero_eq_zero.
+note: this linter can be disabled with `set_option linter.existingAttributeWarning false`
+-/
+#guard_msgs in
+@[simp, reduce_mod_char, to_additive]
+lemma one_eq_one {α : Type*} [One α] : (1 : α) = 1 := rfl
+
+@[to_additive (attr := reduce_mod_char, simp)]
+lemma one_eq_one' {α : Type*} [One α] : (1 : α) = 1 := rfl