Syntax and Macros🔗

In Lean, code is first parsed into syntax, which is then elaborated into expressions. The easiest way to create new tactics, commands and terms is to work at the syntax level, with new syntax mapped to existing syntax. Functions that transform syntax are called macros.

In this chapter we give recipes for matching, creating and transforming syntax.

1. Quasi-Quotes: Creating and Matching Syntax
2. Adding Term Syntax
3. Adding command syntax
4. Adding syntax (categories)