def Lean.Elab.WF.withAppN (n : Nat) (e : Lean.Expr) (k : Array Lean.Expr → Lean.MetaM Lean.Expr) : Lean.MetaM Lean.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 : Lean.Meta.ArgsPacker) (preDefs : Array Lean.Elab.PreDefinition) : Lean.MetaM Lean.Elab.PreDefinition

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