Documentation

Lean.Elab.MacroArgUtil

source
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
    Instances For
      source
      partial def Lean.Elab.Command.expandMacroArg.mkSyntaxAndPat (id? : Option Ident) (id : Term) (stx : TSyntax `stx) :
      CommandElabM (TSyntax `stx × Term)
      source
      def Lean.Elab.Command.expandMacroArg.mkSplicePat (kind : SyntaxNodeKind) (stx : TSyntax `stx) (id : Term) (suffix : String) :
      CommandElabM Term
      Equations
        Instances For
          source
          partial def Lean.Elab.Command.expandMacroArg.mkAntiquotNode :
          TSyntax `stx → Term → CommandElabM Term