Documentation

Lean.Elab.ElabRules

source
def Lean.Elab.Command.elabElabRulesAux (doc? : Option (TSyntax `Lean.Parser.Command.docComment)) (attrs? : Option (Syntax.TSepArray `Lean.Parser.Term.attrInstance ",")) (attrKind : TSyntax `Lean.Parser.Term.attrKind) (k : SyntaxNodeKind) (cat? expty? : Option Ident) (alts : Array (TSyntax `Lean.Parser.Term.matchAlt)) :
CommandElabM Syntax
Instances For
    source
    def Lean.Elab.Command.elabElabRules :
    CommandElab
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Elab.Command.elabElab :
      CommandElab
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For