class ... := too

Author: kmill

Diff for: src/Lean/Elab/Structure.lean

@@ -141,8 +141,9 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str
   if structStx[5][0].isToken ":=" then
     -- https://github.com/leanprover/lean4/issues/5236
     if Linter.getLinterValue Linter.linter.deprecated (← getOptions) then
-      withRef structStx[0] <| withRef structStx[5][0] <| logWarning <| .tagged ``Linter.deprecatedAttr "\
-        'structure ... :=' has been deprecated in favor of 'structure ... where'.\n\
+      let cmd := if structStx[0].getKind == ``Parser.Command.classTk then "class" else "structure"
+      withRef structStx[0] <| withRef structStx[5][0] <| logWarning <| .tagged ``Linter.deprecatedAttr s!"\
+        '{cmd} ... :=' has been deprecated in favor of '{cmd} ... where'.\n\
         You can disable this warning with 'set_option linter.deprecated false'."
   let fieldBinders := if structStx[5].isNone then #[] else structStx[5][2][0].getArgs
   fieldBinders.foldlM (init := #[]) fun (views : Array StructFieldView) fieldBinder => withRef fieldBinder do

Diff for: tests/lean/linterMissingDocs.lean

@@ -53,7 +53,7 @@ structure Foo where
   {mk4 mk5 : Nat}
   [mk6 mk7 : Nat]
 
-class Bar (α : Prop) := mk ::
+class Bar (α : Prop) where mk ::
   (foo bar := 1)
 
 class Bar2 (α : Prop) where

Diff for: tests/lean/run/5236.lean

@@ -2,6 +2,8 @@
 # Deprecate `:=` for `inductive` and `structure`
 -/
 
+set_option linter.deprecated true
+
 /--
 warning: 'inductive ... :=' has been deprecated in favor of 'inductive ... where'.
 You can disable this warning with 'set_option linter.deprecated false'.
@@ -18,3 +20,11 @@ You can disable this warning with 'set_option linter.deprecated false'.
 #guard_msgs in
 structure S :=
   (n : Nat)
+
+/--
+warning: 'class ... :=' has been deprecated in favor of 'class ... where'.
+You can disable this warning with 'set_option linter.deprecated false'.
+-/
+#guard_msgs in
+class C :=
+  (n : Nat)