def
Lean.Elab.Term.Quotation.withNewLocal
{α : Type}
(l : Lake.Name)
(x : Lean.Elab.Term.Quotation.PrecheckM α)
:
Instances For
def
Lean.Elab.Term.Quotation.withNewLocals
{α : Type}
(ls : Array Lake.Name)
(x : Lean.Elab.Term.Quotation.PrecheckM α)
: