opaque Lean.Elab.WF.debug.definition.wf.replaceRecApps : Lean.Option Bool

def Lean.Elab.WF.assignSubsumed (mvars : Array MVarId) : MetaM (Array MVarId)

def Lean.Elab.WF.groupGoalsByFunction (argsPacker : Meta.ArgsPacker) (numFuncs : Nat) (goals : Array MVarId) : MetaM (Array (Array MVarId))

The subgoals, created by mkDecreasingProof, are of the form [data _recApp: rel arg param], where param is the PackMutual'ed parameter of the current function, and thus we can peek at that to know which function is making the call. The close coupling with how arguments are packed and termination goals look like is not great, but it works for now.

def Lean.Elab.WF.solveDecreasingGoals (funNames : Array Name) (argsPacker : Meta.ArgsPacker) (decrTactics : Array (Option DecreasingBy)) (value : Expr) : MetaM Expr

def Lean.Elab.WF.mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (argsPacker : Meta.ArgsPacker) (wfRel : Expr) (funNames : Array Name) (decrTactics : Array (Option DecreasingBy)) (opaqueProof : Bool) : TermElabM Expr