This module contains roughly everything needed to turn mutual n-ary functions into a single unary function, as used by well-founded recursion.

def Lean.Elab.WF.withAppN (n : Nat) (e : Expr) (k : Array Expr → MetaM Expr) : MetaM Expr

Pass the first n arguments of e to the continuation, and apply the result to the remaining arguments. If e does not have enough arguments, it is eta-expanded as needed.

Unlike Meta.etaExpand does not use withDefault.

def Lean.Elab.WF.packCalls (fixedParamPerms : FixedParamPerms) (argsPacker : Meta.ArgsPacker) (funNames : Array Name) (newF e : Expr) : MetaM Expr

Processes the expression and replaces calls to the preDefs with calls to f.

def Lean.Elab.WF.mutualName (fixedParamPerms : FixedParamPerms) (argsPacker : Meta.ArgsPacker) (preDefs : Array PreDefinition) : Name

def Lean.Elab.WF.packMutual (fixedParamPerms : FixedParamPerms) (argsPacker : Meta.ArgsPacker) (preDefs : Array PreDefinition) : MetaM PreDefinition

Creates a single unary function from the given preDefs, using the machinery in the ArgPacker module.

def Lean.Elab.WF.varyingVarNames (fixedParamPerms : FixedParamPerms) (preDefIdx : Nat) (preDef : PreDefinition) : MetaM (Array Name)

Collect the names of the varying variables (excluding the fixed parameters); this also determines the arity for the well-founded translations, and is turned into an ArgsPacker. We use the term to determine the arity, but take the name from the type, for better names in the

fun : (n : Nat) → Nat | 0 => 0 | n+1 => fun n

idiom.

def Lean.Elab.WF.preDefsFromUnaryNonRec (fixedParamPerms : FixedParamPerms) (argsPacker : Meta.ArgsPacker) (preDefs : Array PreDefinition) (unaryPreDefNonRec : PreDefinition) : MetaM (Array PreDefinition)