diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md
index 25f47f3066..5938758ebe 100644
--- a/doc/SUMMARY.md
+++ b/doc/SUMMARY.md
@@ -32,9 +32,10 @@
 <!-- - [Tactics](./tactics.md) -->
 - [Syntax Extensions](./syntax.md)
   - [The `do` Notation](./do.md)
-  - [User-defined notation](./notation.md)
   - [String Interpolation](./stringinterp.md)
+  - [User-Defined Notation](./notation.md)
   - [Macro Overview](./macro_overview.md)
+  - [Elaborators](./elaborators.md)
   - [Examples](./syntax_examples.md)
     - [Balanced Parentheses](./syntax_example.md)
     - [Arithmetic DSL](./metaprogramming-arith.md)
@@ -57,7 +58,6 @@
   - [Thunk](./thunk.md)
   - [Task and Thread](./task.md)
 - [Functions](./functions.md)
-- [Metaprogramming](./metaprogramming.md)
 
 # Other
 
diff --git a/doc/elaborators.md b/doc/elaborators.md
new file mode 100644
index 0000000000..17e6d9f7f1
--- /dev/null
+++ b/doc/elaborators.md
@@ -0,0 +1,8 @@
+## Elaborators
+
+TODO. See [Lean Together 2021: Metaprogramming in Lean
+4](https://youtu.be/hxQ1vvhYN_U) for an overview as well [the
+continuation](https://youtu.be/vy4JWIiiXSY) about tactic programming.
+For more information on antiquotations, see also §4.1 of [Beyond
+Notations: Hygienic Macro Expansion for Theorem Proving
+Languages](https://arxiv.org/pdf/2001.10490.pdf#page=11).
diff --git a/doc/metaprogramming.md b/doc/metaprogramming.md
deleted file mode 100644
index a78d180d00..0000000000
--- a/doc/metaprogramming.md
+++ /dev/null
@@ -1,10 +0,0 @@
-# Metaprogramming
-
-Macros are a language feature that allows writing code that writes other code (metaprogramming).
-
-In Lean 4, macros are used pervasively. So much so that core language features such as `do` notation
-is implemented via macros! As a language user, macros are useful to easily
-embed domain-specific languages and to generate code at compile-time, to name a few uses.
-
-## References
-- [Hygenic Macro Expansion for Theorem Proving Languages](https://arxiv.org/abs/2001.10490)
diff --git a/doc/syntax.md b/doc/syntax.md
index df0ec10986..e6a3a527c9 100644
--- a/doc/syntax.md
+++ b/doc/syntax.md
@@ -1,14 +1,15 @@
 # Syntax Extensions
 
-[Lean's syntax](lexical_structure.md) can be extended and customized
-by users at every level, ranging from basic "mixfix" notations to
-custom elaborators. In fact, all builtin syntax is parsed and
+Lean's syntax can be extended and customized
+by users at every level, ranging from [basic "mixfix" notations](./notation.md)
+over [macro transformers](./macro_overview.md) to
+[type-aware elaborators](./elaborators.md). In fact, all builtin syntax is parsed and
 processed using the same mechanisms and APIs open to users. In this
 section, we will describe and explain the various extension points.
 Significant syntax extensions already builtin into Lean such as the
 [`do` notation](./do.md) are described in subsections.
 
-While [introducing new notations](./notation.md) is a relatively rare feature in
+While introducing new syntax is a relatively rare feature in
 programming languages and sometimes even frowned upon because of its
 potential to obscure code, it is an invaluable tool in formalization
 for expressing established conventions and notations of the respective
@@ -17,14 +18,3 @@ to factor out common boilerplate code into (well-behaved) macros and
 to embed entire custom domain specific languages (DSLs) to textually
 encode subproblems efficiently and readably can be of great benefit to
 both programmers and proof engineers alike.
-
-## Syntax and Macros
-
-## Elaborators
-
-TODO. See [Lean Together 2021: Metaprogramming in Lean
-4](https://youtu.be/hxQ1vvhYN_U) for an overview as well [the
-continuation](https://youtu.be/vy4JWIiiXSY) about tactic programming.
-For more information on antiquotations, see also §4.1 of [Beyond
-Notations: Hygienic Macro Expansion for Theorem Proving
-Languages](https://arxiv.org/pdf/2001.10490.pdf#page=11).