def Lean.Elab.Command.elabMacroRulesAux (doc? : Option (Lean.TSyntax (Lean.Name.mkStr4 "Lean" "Parser" "Command" "docComment"))) (attrs? : Option (Lean.Syntax.TSepArray (Lean.Name.mkStr4 "Lean" "Parser" "Term" "attrInstance") ",")) (attrKind : Lean.TSyntax (Lean.Name.mkStr4 "Lean" "Parser" "Term" "attrKind")) (tk : Lean.Syntax) (k : Lean.SyntaxNodeKind) (alts : Array (Lean.TSyntax (Lean.Name.mkStr4 "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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.