chore: update tests

Author: jrr6

tests/lean/1363.lean.expected.out

@@ -1,5 +1,5 @@
-1363.lean:4:2-4:14: error: invalid use of `[macro_inline]` attribute at `f`, it is not supported in this kind of declaration, declaration must be a non-recursive definition
-1363.lean:9:2-9:14: error: invalid use of `[macro_inline]` attribute at `g`, it is not supported in this kind of declaration, declaration must be a non-recursive definition
-1363.lean:15:2-15:14: error: invalid use of `[macro_inline]` attribute at `h._unary`, it is not supported in this kind of declaration, declaration must be a non-recursive definition
-1363.lean:15:2-15:14: error: invalid use of `[macro_inline]` attribute at `h`, it is not supported in this kind of declaration, declaration must be a non-recursive definition
-1363.lean:21:2-21:14: error: invalid use of `[macro_inline]` attribute at `skipMany`, it is not supported in this kind of declaration, declaration must be a non-recursive definition
+1363.lean:4:2-4:14: error: Cannot add `[macro_inline]` attribute to `f`: This attribute does not support this kind of declaration; only non-recursive definitions are supported
+1363.lean:9:2-9:14: error: Cannot add `[macro_inline]` attribute to `g`: This attribute does not support this kind of declaration; only non-recursive definitions are supported
+1363.lean:15:2-15:14: error: Cannot add `[macro_inline]` attribute to `h._unary`: This attribute does not support this kind of declaration; only non-recursive definitions are supported
+1363.lean:15:2-15:14: error: Cannot add `[macro_inline]` attribute to `h`: This attribute does not support this kind of declaration; only non-recursive definitions are supported
+1363.lean:21:2-21:14: error: Cannot add `[macro_inline]` attribute to `skipMany`: This attribute does not support this kind of declaration; only non-recursive definitions are supported

tests/lean/inductive1.lean.expected.out

@@ -18,7 +18,7 @@ inductive1.lean:69:2-69:5: error: 'Boo.T1.bla' has already been declared
 inductive1.lean:73:10-73:12: error: 'Boo.T1' has already been declared
 inductive1.lean:80:0-80:27: error: invalid use of 'partial' in inductive declaration
 inductive1.lean:81:0-81:33: error: invalid use of 'noncomputable' in inductive declaration
-inductive1.lean:82:2-82:8: error: declaration is not a definition 'T1''
+inductive1.lean:82:2-82:8: error: Cannot add attribute `[inline]`: Declaration `T1'` is not a definition
 inductive1.lean:85:0-85:17: error: invalid 'private' constructor in a 'private' inductive datatype
 inductive1.lean:93:7-93:26: error: invalid inductive type, cannot mix unsafe and safe declarations in mutually inductive datatypes
 inductive1.lean:100:0-100:4: error: Missing resulting type for constructor 'T1.z2': Its resulting type must be specified because it is part of an inductive family declaration

tests/lean/nonfatalattrs.lean.expected.out

@@ -1,4 +1,4 @@
-nonfatalattrs.lean:6:2-6:19: error: unknown attribute [attrUnimplementedattr]
+nonfatalattrs.lean:6:2-6:19: error: Unknown attribute `[attrUnimplementedattr]`
 foo : Nat
 nonfatalattrs.lean:11:12-11:17: error: invalid 'class', declaration 'bar.bar' must be inductive datatype, structure, or constant
 bar : Nat

tests/lean/run/3643.lean

@@ -90,7 +90,7 @@ end Ex2
 section Ex3
 
 -- TODO: allow 'scoped' here? The limitation is in attribute processing itself, not the 'ext' attribute.
-/-- error: scoped attributes must be used inside namespaces -/
+/-- error: Scoped attributes must be used inside namespaces -/
 #guard_msgs in
 @[scoped ext] structure S3' (α β : Type _) where
   a : α

tests/lean/run/reducibilityAttrValidation.lean

@@ -84,7 +84,7 @@ Note: Use `set_option allowUnsafeReducibility true` to override reducibility sta
 #guard_msgs in
 attribute [irreducible] Nat.add
 
-/-- error: scoped attributes must be used inside namespaces -/
+/-- error: Scoped attributes must be used inside namespaces -/
 #guard_msgs in
 attribute [scoped reducible] Nat.add
 

tests/lean/scopedInstanceOutsideNamespace.lean.expected.out

@@ -1,4 +1,4 @@
-scopedInstanceOutsideNamespace.lean:1:0-2:38: error: scoped attributes must be used inside namespaces
+scopedInstanceOutsideNamespace.lean:1:0-2:38: error: Scoped attributes must be used inside namespaces
 "true"
-scopedInstanceOutsideNamespace.lean:6:0-6:30: error: scoped attributes must be used inside namespaces
-scopedInstanceOutsideNamespace.lean:8:2-8:17: error: scoped attributes must be used inside namespaces
+scopedInstanceOutsideNamespace.lean:6:0-6:30: error: Scoped attributes must be used inside namespaces
+scopedInstanceOutsideNamespace.lean:8:2-8:17: error: Scoped attributes must be used inside namespaces

tests/lean/scopedMacros.lean.expected.out

@@ -1,10 +1,10 @@
 10 + 1 : Nat
 scopedMacros.lean:11:7-11:11: error: unknown identifier 'foo!'
 10 + 1 : Nat
-scopedMacros.lean:19:7-19:50: error: scoped attributes must be used inside namespaces
+scopedMacros.lean:19:7-19:50: error: Scoped attributes must be used inside namespaces
 scopedMacros.lean:19:7-19:50: error: invalid syntax node kind 'termBla!_'
 scopedMacros.lean:29:7-29:11: error: unknown identifier 'bla!'
-scopedMacros.lean:36:7-36:45: error: scoped attributes must be used inside namespaces
+scopedMacros.lean:36:7-36:45: error: Scoped attributes must be used inside namespaces
 10 + 20 : Nat
 scopedMacros.lean:47:7-47:14: error: elaboration function for 'termBar!_' has not been implemented
   bar! 10