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
  • One or more equations did not get rendered due to their size.
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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      partial def Lean.Elab.Command.expandMacroArg.mkAntiquotNode :
      TSyntax `stx → Term → CommandElabM Term