The basic data type and namespace for the Lean.Meta.ArgsPacker modules.

This is separated so that Lean.Elab.PreDefinition.WF.Eqns can include the type in EqnInfos without depending on full module with operations.

structure Lean.Meta.ArgsPacker : Type

The metadata required for the operation in the Lean.Meta.ArgsPacker module; see the module docs there for an overview.

• varNamess : Array (Array Lake.Name)

  Variable names to use when unpacking a packed argument.

  Crucially, the size of this array also indicates the number of functions to pack, and the length of each array the arity.

instance Lean.Meta.instInhabitedArgsPacker : Inhabited Lean.Meta.ArgsPacker

Equations

• Lean.Meta.instInhabitedArgsPacker = { default := { varNamess := default } }