Auxiliary inductive datatype for combining unelaborated syntax
and already elaborated expressions. It is used to elaborate applications.
Named arguments created using the notation (x := val)
(x := val)
Add a new named argument to namedArgs, and throw an error if it already contains a named argument
with the same name.