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

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

Equations

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

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.

Equations

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

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

Equations

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

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

Equations

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