Metaprogramming & DSL Construction

## Metaprogramming & DSL Construction

The biggest gap. Lean 4 was redesigned around extensible syntax — this is its
killer feature for programming.

- **`macro`**: define compile-time syntax transformations. The simplest way to
create custom notation, control-flow constructs, or domain-specific syntax.
- **`syntax` and `elab`**: define entirely new syntactic categories and their
elaborators. This is how `do`-notation and `∑` notation were built — users
can build the same class of extensions.
- **`elab` commands**: create new top-level commands (like `#eval` or `#check`
but for your own domain).
- **`macro_rules`**: extend an existing macro with additional cases without
modifying the original definition.
- **`quote` / `unquote` / `TSyntax`**: manipulate concrete syntax trees
programmatically — `TSyntax` is the AST type, `quote` embeds it back into
code.
- **`Lean.Elab.Command`**: run elaboration steps from within metaprogramming
code (useful for code generators and custom tooling).
- **`deriving` handlers**: write your own `deriving MyClass` generator so users
can auto-derive instances for your type classes.
- **Custom notation**: `infix`, `infixl`, `infixr`, `notation` for defining
operators and symbolic syntax like `x ⊕ y` or `⟦x⟧`.