return to top
source
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)
If true, then make all parameters that depend on this one become implicit. This is used for projection notation, since structure parameters might be explicit for classes.
true
Add a new named argument to namedArgs, and throw an error if it already contains a named argument with the same name.
namedArgs