# Documentation

Lean.Elab.Arg

• stx:
• expr:

Auxiliary inductive datatype for combining unelaborated syntax and already elaborated expressions. It is used to elaborate applications.

Instances For

Named arguments created using the notation (x := val)

Instances For
Equations
def Lean.Elab.Term.addNamedArg (namedArgs : ) (namedArg : Lean.Elab.Term.NamedArg) :

Add a new named argument to namedArgs, and throw an error if it already contains a named argument with the same name.

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