def Lean.Elab.Command.expandMacroArg (stx : Lean.TSyntax (Lean.Name.mkStr4 "Lean" "Parser" "Command" "macroArg")) : Lean.Elab.Command.CommandElabM (Lean.TSyntax (Lean.Name.mkStr1 "stx") × Lean.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.

partial def Lean.Elab.Command.expandMacroArg.mkSyntaxAndPat (id? : Option Lean.Ident) (id : Lean.Term) (stx : Lean.TSyntax (Lean.Name.mkStr1 "stx")) : Lean.Elab.Command.CommandElabM (Lean.TSyntax (Lean.Name.mkStr1 "stx") × Lean.Term)

def Lean.Elab.Command.expandMacroArg.mkSplicePat (kind : Lean.SyntaxNodeKind) (stx : Lean.TSyntax (Lean.Name.mkStr1 "stx")) (id : Lean.Term) (suffix : String) : Lean.Elab.Command.CommandElabM Lean.Term

Equations

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

partial def Lean.Elab.Command.expandMacroArg.mkAntiquotNode : Lean.TSyntax (Lean.Name.mkStr1 "stx") → Lean.Term → Lean.Elab.Command.CommandElabM Lean.Term