HepLean 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)

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 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.
    Instances For
      source
      partial def Lean.Elab.Command.expandMacroArg.mkAntiquotNode :
      Lean.TSyntax `stx → Lean.Term → Lean.Elab.Command.CommandElabM Lean.Term