Documentation

Lean.Elab.ElabRules

source
def Lean.Elab.Command.withExpectedType (expectedType? : Option Lean.Expr) (x : Lean.Expr → Lean.Elab.TermElabM Lean.Expr) :
Lean.Elab.TermElabM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Command.elabElabRulesAux (doc? : Option (Lean.TSyntax `Lean.Parser.Command.docComment)) (attrKind : Lean.TSyntax `Lean.Parser.Term.attrKind) (k : Lean.SyntaxNodeKind) (cat? : Option Lean.Ident) (expty? : Option Lean.Ident) (alts : Array (Lean.TSyntax `Lean.Parser.Term.matchAlt)) :
Lean.Elab.Command.CommandElabM Lean.Syntax
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Command.elabElabRules:
Lean.Elab.Command.CommandElab
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Command.elabElab:
Lean.Elab.Command.CommandElab
Equations
  • One or more equations did not get rendered due to their size.