Make Lean.Elab.Term.extractBind public.

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

Equations

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

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")

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