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