Documentation

Qq.ForLean.Do

Make Lean.Elab.Term.extractBind public.

source
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.
Instances For
    source
    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.
    Instances For
      source
      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)