diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md
index cb4e5575d4..10260b43b3 100644
--- a/doc/SUMMARY.md
+++ b/doc/SUMMARY.md
@@ -35,7 +35,9 @@
   - [User-defined notation](./notation.md)
   - [String Interpolation](./stringinterp.md)
   - [Macro Overview](./macro_overview.md)
-  - [A Guided Example](./syntax_example.md)
+  - [Examples](./syntax_examples.md)
+    - [Parenthesized Terms](./syntax_example.md)
+    - [Arithmetic DSL](./tutorial/metaprogramming-arith.md)
 - [Declaring New Types](./decltypes.md)
   - [Enumerated Types](./enum.md)
   - [Inductive Types](./inductive.md)
diff --git a/doc/tutorial/metaprogramming-arith.md b/doc/tutorial/metaprogramming-arith.md
index e7de22377c..ed399b8873 100644
--- a/doc/tutorial/metaprogramming-arith.md
+++ b/doc/tutorial/metaprogramming-arith.md
@@ -1,4 +1,4 @@
-## Arithmetic as an embedded domain-specific language
+# Arithmetic as an embedded domain-specific language
 
 Let's parse another classic grammar, the grammar of arithmetic expressions with
 addition, multiplication, integers, and variables.  In the process, we'll learn