Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages

This article introduces a macro expansion algorithm for Interactive Theorem Provers based on Scheme's hygienic macros and adapted for use in proof contexts.

With some improvements and modifications, this algorithm is part of the meta-programming system of Lean 4; it is what allows complex syntactic transformations in a context where safety/correctness is crucial.

A more broad overview of Lean's metaprogramming can be found in [0], but the algorithm is of independent interest and language developers may be interested in studying it.

[0] https://leanprover-community.github.io/lean4-metaprogramming...

Syntactic sugar causes the cancer of semicolon.

The cure is daily s-expression.