RFC: `elab_inline` attribute to inline functions during elaboration

Mathlib sometimes uses local notation to create abbreviations that are even more transparent than abbrev. For example, one module uses local notation "reC" => @IsROrC.re ℂ _ so that the lemmas that use it are in terms of IsROrC directly.

To make these notation-based abbreviations elaborate like functions, we could make them actually be functions and then have an elab_inline attribute that the application elaborator uses to decide whether to unfold a definition. For example, the reC local notation could instead be written as

@[elab_inline] def reC (x : ℂ) := IsROrC.re x

The name elab_inline is meant to be an analogue of inline, but where the inlining occurs at elaboration time rather than compile time.

Below, I have a macro-based implementation for the feature. A simple test of it is

@[elab_inline]
def f (x : Nat) := 2 * x

#check f 37
-- 2 * 37 : Nat

Here is a justification for asking for a change in core Lean rather than using the macro implementation: My implementation suffers from the fact that the elab_inline feature works by creating macro_rules to insert a custom syntax with a custom term elaborator, so it doesn't work well with namespaces or open. Modifying the application elaborator to support such an attribute would make it more reliable.

import Lean
import Std.Lean.Command

open Lean Meta Elab

syntax (name := unfold) "unfold% " ident term:max* : term

@[term_elab unfold] def elabUnfold : Elab.Term.TermElab := fun stx expectedType? => do
  match stx with
  | `(unfold% $f $[$args]*) =>
    -- Note: this doesn't seem to add terminfo to `f`
    let some f ← Term.resolveId? f (withInfo := true) | throwUnknownConstant f.getId
    let e ← Term.elabAppArgs f #[] (args.map .stx) expectedType?
      (explicit := false) (ellipsis := false)
    unfoldDefinition e
  | _ => throwUnsupportedSyntax

/-- Causes the definition to be unfolded during elaboration. -/
syntax (name := elab_inline) "elab_inline" : attr

initialize registerBuiltinAttribute {
  name := `elab_inline
  descr := ""
  add := fun src ref kind => do
    if (kind != AttributeKind.global) then
      throwError "`elab_inline` can only be used as a global attribute"
    liftCommandElabM <| withRef ref <| Command.elabCommand (← `(command|
      macro_rules
      | `($(mkIdent src)) => `(unfold% $(mkIdent src))
      | `($(mkIdent src) $$args*) => `(unfold% $(mkIdent src) $$args*))) }

Start by locating Lean's application elaborator and compare it with the macro-based implementation included in the issue. Verify the proposed attribute with the shown reC and f examples, including namespace and open behavior; done means elaboration-time unfolding works reliably without the macro workaround.