Make `Lean.Elab.Term.extractBind` public.

source
def Lean.Elab.Term.mkIdBindFor (type : Expr) :
TermElabM ExtractMonadResult
Equations

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

Instances For

source
def Lean.Elab.Term.extractBind (expectedType? : Option Expr) :
TermElabM ExtractMonadResult
Equations

- One or more equations did not get rendered due to their size.
- Lean.Elab.Term.extractBind none = Lean.throwError (Lean.toMessageData "invalid 'do' notation, expected type is not available")

Instances For