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.

def Lean.Elab.WF.packMutual (fixedPrefix : Nat) (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.