RFC: Field attributes

Proposal

Structure fields in Lean generate projection functions, but it is currently impossible to attach attributes to those projections at the point of declaration. Any attribute on a field is rejected with "Invalid attribute: Attributes cannot be added to fields". This proposal lifts that restriction and makes it so that users can annotate fields directly instead of writing separate attribute commands after the structure:

-- Today you must write this separately:
structure Config where
  oldField : Nat
  normalize : String → String
attribute [deprecated "Use newField instead"] Config.oldField
attribute [simp] Config.normalize

-- With this proposal:
structure Config where
  @[deprecated "Use newField instead"] oldField : Nat
  @[simp] normalize : String → String

This also enables metadata attributes like a serde-style pattern where attributes annotate fields for deriving handlers rather than affecting the projection's elaboration behavior:

initialize jsonField : ParametricAttribute String
  registerParametricAttribute `json_rename ...

structure User where
  @[json_rename "user_name"] userName : String
  @[json_rename "email_address"] email : String

I think this is great for projects using deriving for serialization (JSON, binary formats, ORMs), documentation generators that want structured per-field metadata and any user who wants @[simp], @[inline], or @[deprecated] on a specific projection without a post-hoc attribute command. The pattern is familiar to users coming from Rust (#[serde(...)]), Haskell (field annotations) and Java/Kotlin (annotation processors).

The implementation is minimal, the change removes two lines from checkValidFieldModifier and adds five lines to the finalize step in Structure.lean, following the identical pattern already used for applying docstrings to field projections. No new persistent storage or data types are needed since attributes are applied to the projection declaration via the existing Term.applyAttributes infrastructure, exactly as they would be if written as a standalone attribute command after the structure.

Community Feedback

Discussed on Lean Zulip: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Field.20attributes/with/582642404. No replies at time of submission and no prior issues found on this specific feature.

A prototype implementation is available at SrGaabriel/lean4 with tests passing on CI.

Start in Structure.lean by reviewing checkValidFieldModifier and the structure finalization step, following the existing pattern for applying docstrings to field projections. Use the prototype and its CI tests as a reference; done means declaration-site attributes are accepted and applied to generated projections, including metadata attributes.