Documentation

Lean.Elab.MacroArgUtil

source
def Lean.Elab.Command.expandMacroArg (stx : Lean.TSyntax `Lean.Parser.Command.macroArg) :
Lean.Elab.Command.CommandElabM (Lean.TSyntax `stx × Lean.Term)
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Elab.Command.expandMacroArg.mkSyntaxAndPat (id? : Option Lean.Ident) (id : Lean.Term) (stx : Lean.TSyntax `stx) :
Lean.Elab.Command.CommandElabM (Lean.TSyntax `stx × Lean.Term)
source
def Lean.Elab.Command.expandMacroArg.mkSplicePat (kind : Lean.SyntaxNodeKind) (stx : Lean.TSyntax `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.
source
partial def Lean.Elab.Command.expandMacroArg.mkAntiquotNode:
Lean.TSyntax `stx → Lean.Term → Lean.Elab.Command.CommandElabM Lean.Term