Elaboration: Extending Syntax🔗

The easiest way to extend the syntax of Lean is to write macros that transform new syntax into existing syntax (see Syntax and Macros). However, a more powerful way to extend the syntax of Lean is to write new elaborators that transform new syntax into expressions. In this chapter we give recipes for writing elaborators for new syntax for terms and commands.

Recipes:

1. Adding Syntax for terms
2. Adding syntax for commands