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.

def Lean.Elab.Command.elabElabRulesAux (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")) (k : Lean.SyntaxNodeKind) (cat? : Option Lean.Ident) (expty? : Option Lean.Ident) (alts : Array (Lean.TSyntax (Lean.Name.mkStr4 "Lean" "Parser" "Term" "matchAlt"))) : Lean.Elab.Command.CommandElabM Lean.Syntax

Equations

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

def Lean.Elab.Command.elabElabRules : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabElab : Lean.Elab.Command.CommandElab

Equations

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