def Lean.Elab.Command.elabMacroRulesAux (doc? : Option (Lean.TSyntax `Lean.Parser.Command.docComment)) (attrs? : Option (Lean.Syntax.TSepArray `Lean.Parser.Term.attrInstance ",")) (attrKind : Lean.TSyntax `Lean.Parser.Term.attrKind) (tk : Lean.Syntax) (k : Lean.SyntaxNodeKind) (alts : Array (Lean.TSyntax `Lean.Parser.Term.matchAlt)) : Lean.Elab.Command.CommandElabM Lean.Syntax

Remark: k is the user provided kind with the current namespace included. Recall that syntax node kinds contain the current namespace.

def Lean.Elab.Command.elabMacroRules : Lean.Elab.Command.CommandElab