Lean.Elab.PreDefinition.WF.PackMutual

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

source

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.

Equations

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

source

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.

Equations

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

source

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

Name

Equations

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

source

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.

Equations

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

source

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.

Equations

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

source

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

MetaM (Array PreDefinition)

Equations

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