Documentation

Qq.ForLean.Do

Make Lean.Elab.Term.extractBind public.

source
def Lean.Elab.Term.mkIdBindFor (type : Expr) :
TermElabM ExtractMonadResult
Equations
    Instances For
      source
      def Lean.Elab.Term.extractBind (expectedType? : Option Expr) :
      TermElabM ExtractMonadResult
      Equations
        Instances For
          source
          partial def Lean.Elab.Term.extractBind.extract? (extractStep? : Expr → MetaM (Option ExtractMonadResult)) (type : Expr) :
          MetaM (Option ExtractMonadResult)