Auxiliary inductive datatype for combining unelaborated syntax and already elaborated expressions. It is used to elaborate applications.
Equations
- Lean.Elab.Term.instInhabitedArg = { default := Lean.Elab.Term.Arg.stx default }
Named arguments created using the notation (x := val)
.