Factoring out declarations with a macro

Stream: lean4

[Son Ho]

I'm trying to write a macro to factor out declarations with similar bodies. Here is a minimal example:

-- This command:
generic (x1, x2) def «%» := 0

/- Should generate:
def x1 := 0
def x2 := 0
-/

To support this minimal example, I managed to write the following custom elaboration (I simply explore the syntax tree and replace the string "%" whenever it appears in a name):

import Lean
open Lean Elab Command Term Meta

/-!
The trick is simple: we explore the syntax and replace `"%"` whenever it appears inside a name.
-/

def elabName (new : String) (n : Name) : Name :=
  match n with
  | .anonymous => .anonymous
  | .str pre str =>
    -- The special case: we replace occurrences of `%`
    let str := if str == "%" then new else str
    .str (elabName new pre) str
  | .num pre i => (.num (elabName new pre) i)

def elabCommand (name : String) (stx : Syntax) : Syntax :=
  match stx with
  | .missing => .missing
  | .node info kind args => .node info kind (args.map (elabCommand name))
  | .atom info val => .atom info val
  | .ident info rawVal val preresolved =>
    .ident info rawVal (elabName name val) preresolved

def elabCommands (names : Array String) (cmd : TSyntax `command) : CommandElabM Unit := do
  let elabOne (name : String) := do
    let cmd := elabCommand name cmd
    logInfo m!"cmd: {cmd}"
    Lean.Elab.Command.elabCommand cmd
  names.forM elabOne

syntax (name := genericCommand) "generic" "(" ident,* ")" command : command

@[command_elab genericCommand]
def genericCommandImpl : CommandElab := fun stx => do
  match stx with
  | `(genericCommand| generic ( $ids,* ) $stx) =>
    let ids := ids.getElems.map fun id =>
      match id.raw.getId with
      | .str .anonymous id => id
      | _ => ""
    logInfo m!"ids: {ids}"
    logInfo m!"stx: {stx}"
    elabCommands ids stx
  | _ => throwUnsupportedSyntax

This is a bit of a hack, but works with the caveat that when I define more than one theorem at once, the goto definition only works for the last declaration:

-- Definitions: ok
generic (x1, x2) def «%» := 0
#print x1 -- `def x1 : Nat := 0` - Can goto def
#print x2 -- `def x2 : Nat := 0` - Can goto def

-- One theorem: ok
generic (th1) theorem «%» : True := by simp
#check th1 -- Can goto def

-- More than one theorem: not ok
generic (th2, th3) theorem «%» : True := by simp
#check th2 -- **HERE**: can't goto def
#check th3 -- Can goto def

Does someone has an idea about what's going on? I dived into the code of elabDeclaration but I don't manage to figure what I do wrong and where the discrepancy comes from.