Make Lean.Elab.Term.extractBind
public.
Instances For
Instances For
partial def
Lean.Elab.Term.extractBind.extract?
(extractStep? : Lean.Expr → Lean.MetaM (Option Lean.Elab.Term.ExtractMonadResult))
(type : Lean.Expr)
:
Qq.ForLean.Do
Make Lean.Elab.Term.extractBind
public.