core.init.meta.pexpr
Quoted expressions. They can be converted into expressions by using a tactic.
Choice macros are used to implement overloading.
Information about unelaborated structure instance expressions.
Create a structure instance expression.