Make Lean.Elab.Term.extractBind public.

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

Equations

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

def Lean.Elab.Term.extractBind (expectedType? : Option Lean.Expr) : Lean.Elab.TermElabM Lean.Elab.Term.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")

partial def Lean.Elab.Term.extractBind.extract? (extractStep? : Lean.Expr → Lean.MetaM (Option Lean.Elab.Term.ExtractMonadResult)) (type : Lean.Expr) : Lean.MetaM (Option Lean.Elab.Term.ExtractMonadResult)