def
Lean.Elab.withCommonTelescope
{α : Type}
(preDefs : Array Lean.Elab.PreDefinition)
(k : Array Lean.Expr → Array Lean.Expr → Lean.Elab.TermElabM α)
:
Instances For
Instances For
def
Lean.Elab.wfRecursion
(preDefs : Array Lean.Elab.PreDefinition)
(wf? : Option Lean.Elab.WF.TerminationWF)
(decrTactic? : Option Lean.Syntax)
: