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.

## Instances For

def
Lean.Elab.WF.packMutual
(fixedPrefix : Nat)
(argsPacker : Lean.Meta.ArgsPacker)
(preDefs : Array Lean.Elab.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.