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

Equations

• One or more equations did not get rendered due to their size.