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

Equations

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