def
Lean.Elab.WF.elabWFRel
{α : Type}
(preDefs : Array Lean.Elab.PreDefinition)
(unaryPreDefName : Lake.Name)
(fixedPrefixSize : Nat)
(argType : Lean.Expr)
(wf : Lean.Elab.WF.TerminationWF)
(k : Lean.Expr → Lean.Elab.TermElabM α)
:
Equations
- One or more equations did not get rendered due to their size.