13. Notations and Macros🔗

Different mathematical fields have their own notational conventions, and many notations are re-used with differing meanings in different fields. It is important that formal developments are able to use established notations: formalizing mathematics is already difficult, and the mental overhead of translating between syntaxes can be substantial. At the same time, it's important to be able to control the scope of notational extensions. Many fields use related notations with very different meanings, and it should be possible to combine developments from these separate fields in a way where both readers and the system know which convention is in force in any given region of a file.

Lean addresses the problem of notational extensibility with a variety of mechanisms, each of which solves a different aspect of the problem. They can be combined flexibly to achieve the necessary results:

  • The extensible parser allows a great variety of notational conventions to be implemented declaratively, and combined flexibly.

  • Macros allow new syntax to be easily mapped to existing syntax, which is a simple way to provide meaning to new constructs. Due to hygiene and automatic propagation of source positions, this process doesn't interfere with Lean's interactive features.

  • Elaborators provide new syntax with the same tools available to Lean's own syntax in cases where a macro is insufficiently expressive.

  • Notations allow the simultaneous definition of a parser extension, a macro, and a pretty printer. When defining infix, prefix, or postfix operators, custom operators automatically take care of precedence and associativity.

  • Low-level parser extensions allow the parser to be extended in ways that modify its rules for tokens and whitespace, or that even completely replace Lean's syntax. This is an advanced topic that requires familiarity with Lean internals; nevertheless, the possibility of doing this without modifying the compiler is important. This reference manual is written using a language extension that replaces Lean's concrete syntax with a Markdown-like language for writing documents, but the source files are still Lean files.

  1. 13.1. Custom Operators
  2. 13.2. Precedence
  3. 13.3. Notations
    1. 13.3.1. Operators and Notations
  4. 13.4. Defining New Syntax
    1. 13.4.1. Syntax Model
    2. 13.4.2. Syntax Node Kinds
    3. 13.4.3. Token and Literal Kinds
    4. 13.4.4. Internal Kinds
    5. 13.4.5. Source Positions
    6. 13.4.6. Inspecting Syntax
    7. 13.4.7. Typed Syntax
    8. 13.4.8. Aliases
    9. 13.4.9. Helpers for Typed Syntax
    10. 13.4.10. Syntax Categories
    11. 13.4.11. Syntax Rules
    12. 13.4.12. Indentation
  5. 13.5. Macros
    1. 13.5.1. Hygiene
    2. 13.5.2. The Macro Monad
      1. 13.5.2.1. Exceptions and Errors
      2. 13.5.2.2. Hygiene-Related Operations
      3. 13.5.2.3. Querying the Environment
    3. 13.5.3. Quotation
      1. 13.5.3.1. Quasiquotation
      2. 13.5.3.2. Splices
      3. 13.5.3.3. Token Antiquotations
    4. 13.5.4. Matching Syntax
    5. 13.5.5. Defining Macros
      1. 13.5.5.1. The macro_rules Command
      2. 13.5.5.2. The macro Command
      3. 13.5.5.3. The Macro Attribute
  6. 13.6. Elaborators