Understand and react to Lean 4's hygienic macro expansion

[masak]

It sounds very good:

Lean 3’s "mixfix" notation system is still supported in Lean 4, but based on the much more general macro system; in fact, the Lean 3 notation keyword itself has been reimplemented as a macro, more specifically as a macro-generating macro. By providing such a tower of abstractions for writing syntax sugars, of which we will see more levels below, we want to enable users to work in the simplest model appropriate for their respective use case while always keeping open the option to switch to a lower, more expressive level.

[...]

macro itself is another command-level macro that, for our notation example, expands to two commands [...] that is, a pair of parser extension and syntax transformer. By separating these two steps at this abstraction level, it becomes possible to define (mutually) recursive macros and to reuse syntax between macros. Using macro_rules, users can even extend existing macros with new rules. In general, separating parsing and expansion means that that we can obtain a well-structured syntax tree pre-expansion, i.e. a concrete syntax tree, and use it to implement source code tooling such as auto-completion, go-to-definition, and refactorings.

Closeable upon understanding all this at a sufficient depth, and maybe also deciding which bits to be inspired by.