feat: allow attributes on structure fields

src/Lean/Elab/Structure.lean

@@ -324,8 +324,6 @@ def checkValidFieldModifier (modifiers : Modifiers) : TermElabM Unit := do
     throwError "Invalid modifier: Fields cannot be marked as `partial`"
   if modifiers.isUnsafe then
     throwError "Invalid modifier: Fields cannot be marked as `unsafe`"
-  if modifiers.attrs.size != 0 then
-    throwError "Invalid attribute: Attributes cannot be added to fields"
 
 /-
 ```
@@ -1576,6 +1574,11 @@ def elabStructureCommand : InductiveElabDescr where
                         if isClass (← getEnv) parentName then
                           setReducibilityStatus fieldInfo.declName .implicitReducible
                     addParentInstances parentInfos
+                  -- Apply field attributes to projection functions
+                  for field in view.fields do
+                    if (← getEnv).contains field.declName then
+                      withRef field.ref do
+                        Term.applyAttributes field.declName field.modifiers.attrs
                   -- Add field docstrings here (after @[class] attribute is applied)
                   -- so that Verso docstrings can use the class.
                   for field in view.fields do

tests/elab/structFieldAttrs.lean

@@ -0,0 +1,35 @@
+-- Tests for attributes on structure fields.
+-- Attributes on fields are applied to the generated projection functions.
+
+import Lean
+
+/-! ### @[deprecated] on a field -/
+
+structure Foo where
+  @[deprecated "Use y instead!" (since := "2025-04-30")] x : Nat
+  y : Bool
+
+/-! ### @[inline] on a field -/
+
+structure Baz where
+  @[inline] compute : Nat → Nat
+
+/-! ### @[reducible] on a class field (class projections are semireducible by default) -/
+
+class MyClass (α : Type) where
+  @[reducible] default : α
+
+/-! ### Field with default -/
+
+structure WithDefault where
+  @[deprecated "Stop!" (since := "2025-04-30")] x : Nat := 42
+
+/-! ### Verify attributes were applied to projections -/
+
+/-- info: true -/
+#guard_msgs in
+#eval do return Lean.Linter.isDeprecated (← Lean.getEnv) ``Foo.x
+
+/-- info: true -/
+#guard_msgs in
+#eval do return Lean.Linter.isDeprecated (← Lean.getEnv) ``WithDefault.x