feat: add deprecated_arg attribute

[wkrozowski]

This PR adds a @[deprecated_arg] attribute that marks individual function parameters as deprecated. When a caller uses the old parameter name, the elaborator emits a deprecation warning with a code action hint to rename or delete the argument, and silently forwards the value to the correct binder.

Supported forms:

• @[deprecated_arg old new (since := "...")] — renamed parameter, warns and forwards
• @[deprecated_arg old new "reason" (since := "...")] — with custom message
• @[deprecated_arg removed (since := "...")] — removed parameter, errors with delete hint
• @[deprecated_arg removed "reason" (since := "...")] — removed with custom message

A warning is emitted if (since := "...") is omitted.

When a parameter is deprecated without a replacement, the elaborator treats it as no longer present: using it as a named argument produces an error. Note that positional uses of deprecated arguments are not checked — if a function's arity changed, the caller will simply get a "function expected" error.

The linter.deprecated.arg option (default true) controls behavior: when enabled, renamed args produce warnings and removed args produce specific deprecation errors with code action hints; when disabled, both fall through to the standard "invalid argument name" error. This lets library authors phase out old parameter names without breaking downstream code immediately.

Example (renamed parameter):

@[deprecated_arg old new (since := "2026-03-18")]
def f (new : Nat) : Nat := new

/--
warning: parameter `old` of `f` has been deprecated, use `new` instead

Hint: Rename this argument:
  o̵l̵d̵n̲e̲w̲
---
info: f 42 : Nat
-/
#guard_msgs in
#check f (old := 42)

Example (removed parameter):

@[deprecated_arg removed (since := "2026-03-18")]
def g (x : Nat) : Nat := x

/--
error: parameter `removed` of `g` has been deprecated

Hint: Delete this argument:
  (̵r̵e̵m̵o̵v̵e̵d̵ ̵:̵=̵ ̵4̵2̵)̵
-/
#guard_msgs in
#check g (removed := 42)

[wkrozowski]

!bench

[leanprover-radar]

Benchmark results for c4cc192 against d9c3bbf are in. There are no significant changes. @wkrozowski

• 🟥 build//instructions: +4.3G (+0.04%)

Small changes (2🟥)

• 🟥 build/module/Init.Notation//instructions: +43.9M (+0.24%)
• 🟥 build/module/Lean.Elab.App//instructions: +590.0M (+1.66%) (reduced significance based on *//lines)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d9c3bbf1b49b5ca33d1cce3d8d185a76969dfcd6 --onto 87180a09c49c91577e54284703c73c5ca76be126. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-20 17:02:51)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5cc6585c9b9b7c80a0a6b3899cfbf46592ca7273 --onto 87180a09c49c91577e54284703c73c5ca76be126. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-20 18:13:34)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5cc6585c9b9b7c80a0a6b3899cfbf46592ca7273 --onto 4bf7fa7447eea00cecba8327bb9c9e5f4485f0a7. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-23 18:15:01)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5cc6585c9b9b7c80a0a6b3899cfbf46592ca7273 --onto e6df474dd9c3ad0e21771eaa808c53f66222216d. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-26 01:08:39)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5cc6585c9b9b7c80a0a6b3899cfbf46592ca7273 --onto 4786e082dca22873d14d2a5b9b7c8843380c6e78. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-26 17:15:55)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase d9c3bbf1b49b5ca33d1cce3d8d185a76969dfcd6 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-20 17:02:53)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5cc6585c9b9b7c80a0a6b3899cfbf46592ca7273 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-20 18:13:36)