def
Lean.Elab.Command.withExpectedType
(expectedType? : Option Lean.Expr)
(x : Lean.Expr → Lean.Elab.TermElabM Lean.Expr)
:
Instances For
def
Lean.Elab.Command.elabElabRulesAux
(doc? : Option (Lean.TSyntax `Lean.Parser.Command.docComment))
(attrs? : Option (Lean.Syntax.TSepArray `Lean.Parser.Term.attrInstance ","))
(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))
: