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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.WF.groupGoalsByFunction (argsPacker : Lean.Meta.ArgsPacker) (numFuncs : Nat) (goals : Array Lean.MVarId) : Lean.MetaM (Array (Array Lean.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 (argsPacker : Lean.Meta.ArgsPacker) (decrTactics : Array (Option Lean.Elab.DecreasingBy)) (value : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

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