def Lean.Elab.Command.expandMacroArg (stx : TSyntax `Lean.Parser.Command.macroArg) : CommandElabM (TSyntax `stx × Term)

Convert macro arg into a syntax command item and a pattern element