diff --git a/README.md b/README.md
index a8d3552..229c7c6 100644
--- a/README.md
+++ b/README.md
@@ -22,6 +22,9 @@ A PDF is [available here for download](../../releases/download/latest/Metaprogra
     1. ...
     2. [Expressions](md/solutions/expressions.md)
     3. [`MetaM`](md/solutions/metam.md)
+    4. [`Syntax`](md/solutions/syntax.md)
+    5. ...
+    6. [Elaboration](md/solutions/elaboration.md)
 
 Sources to extract material from:
 * [Material written by Ed](https://github.com/leanprover-community/mathlib4/blob/tutorial/docs/metaprogramming/02_metavariables.md)
diff --git a/lean/main/elaboration.lean b/lean/main/elaboration.lean
index c65f90a..f39bc98 100644
--- a/lean/main/elaboration.lean
+++ b/lean/main/elaboration.lean
@@ -340,3 +340,60 @@ syntax sugar of the `elab` syntax instead:
 -- This `t` syntax will effectively perform the first two lines of `myanonImpl`
 elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do 
   sorry
+
+
+/-!
+
+## Exercises
+
+1. Consider the following code. Rewrite `syntax` + `@[term_elab hi]... : TermElab` combination using just `elab`.
+
+```
+syntax (name := hi) term " ♥ " " ♥ "? " ♥ "? : term
+
+@[term_elab hi]
+def heartElab : TermElab := fun stx tp =>
+  match stx with
+    | `($l:term ♥) => do
+      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
+      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 1)
+    | `($l:term ♥♥) => do
+      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
+      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 2)
+    | `($l:term ♥♥♥) => do
+      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
+      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 3)
+    | _ =>
+      throwUnsupportedSyntax
+```
+
+2. Here is some syntax taken from a real mathlib command `alias`.
+
+```
+syntax (name := our_alias) (docComment)? "our_alias " ident " ← " ident* : command
+```
+
+We want `alias hi ← hello yes` to print out the identifiers after `←` - that is, "hello" and "yes".
+
+Please add these semantics:
+
+**a)** using `syntax` + `@[command_elab alias] def elabOurAlias : CommandElab`.  
+**b)** using `syntax` + `elab_rules`.  
+**c)** using `elab`.
+
+3. Here is some syntax taken from a real mathlib tactic `nth_rewrite`.
+
+```
+open Parser.Tactic
+syntax (name := nthRewriteSeq) "nth_rewrite " (config)? num rwRuleSeq (ppSpace location)? : tactic
+```
+
+We want `nth_rewrite 5 [←add_zero a] at h` to print out `"rewrite location!"` if the user provided location, and `"rewrite target!"` if the user didn't provide location.
+
+Please add these semantics:
+
+**a)** using `syntax` + `@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic`.  
+**b)** using `syntax` + `elab_rules`.  
+**c)** using `elab`.
+
+-/
diff --git a/lean/main/expressions.lean b/lean/main/expressions.lean
index 1da1b68..2ea52f7 100644
--- a/lean/main/expressions.lean
+++ b/lean/main/expressions.lean
@@ -257,12 +257,12 @@ expressions.
 
 1. Create expression `1 + 2` with `Expr.app`.
 2. Create expression `1 + 2` with `Lean.mkAppN`.
-3. Create expression `λ x => 1 + x`.
-4. [**De Bruijn Indexes**] Create expression `λ a, λ b, λ c, (b * a) + c`.
-5. Create expression `λ x y => x + y`.
-6. Create expression `λ x, String.append "hello, " x`.
+3. Create expression `fun x => 1 + x`.
+4. [**De Bruijn Indexes**] Create expression `fun a, fun b, fun c, (b * a) + c`.
+5. Create expression `fun x y => x + y`.
+6. Create expression `fun x, String.append "hello, " x`.
 7. Create expression `∀ x : Prop, x ∧ x`.
 8. Create expression `Nat → String`.
-9. Create expression `λ (p : Prop) => (λ hP : p => hP)`.
+9. Create expression `fun (p : Prop) => (λ hP : p => hP)`.
 10. [**Universe levels**] Create expression `Type 6`.
 -/
diff --git a/lean/main/metam.lean b/lean/main/metam.lean
index 73d7c03..ee9780f 100644
--- a/lean/main/metam.lean
+++ b/lean/main/metam.lean
@@ -1213,23 +1213,61 @@ Lean parser.
 Notice that changing the type of the metavarible from `Nat` to, for example, `String`, doesn't raise any errors - that's why, as was mentioned, we must make sure *"(a) that `val` must have the target type of `mvarId` and (b) that `val` must only contain `fvars` from the local context of `mvarId`"*.
 2. [**Metavariables**] What would `instantiateMVars (Lean.mkAppN (Expr.const 'Nat.add []) #[mkNatLit 1, mkNatLit 2])` output?
 3. [**Metavariables**] Fill in the missing lines in the following code.
+
+  ```
+  #eval show MetaM Unit from do
+    let oneExpr := Expr.app (Expr.const `Nat.succ []) (Expr.const ``Nat.zero [])
+    let twoExpr := Expr.app (Expr.const `Nat.succ []) oneExpr
+
+    -- Create `mvar1` with type `Nat`
+    -- let mvar1 ← ...
+    -- Create `mvar2` with type `Nat`
+    -- let mvar2 ← ...
+    -- Create `mvar3` with type `Nat`
+    -- let mvar3 ← ...
+
+    -- Assign `mvar1` to `2 + ?mvar2 + ?mvar3`
+    -- ...
+
+    -- Assign `mvar3` to `1`
+    -- ...
+
+    -- Instantiate `mvar1`, which should result in expression `2 + ?mvar2 + 1`
+    ...
+  ```
 4. [**Metavariables**] Consider the theorem `red`, and tactic `explore` below.  
   a) What would be the `type` and `userName` of metavariable `mvarId`?  
   b) What would be the `type`s and `userName`s of all local declarations in this metavariable's local context?  
   Print them all out.
+
+  ```
+  elab "explore" : tactic => do
+    let mvarId : MVarId ← Lean.Elab.Tactic.getMainGoal
+    let metavarDecl : MetavarDecl ← mvarId.getDecl
+
+    IO.println "Our metavariable"
+    -- ...
+
+    IO.println "All of its local declarations"
+    -- ...
+
+  theorem red (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by
+    explore
+    sorry
+  ```
 5. [**Metavariables**] Write a tactic `solve` that proves the theorem `red`.
 6. [**Computation**] What is the normal form of the following expressions:  
-  a) `λ x => x` of type `Bool → Bool`  
-  b) `(λ x => x) ((true && false) || true)` of type `Bool`  
-  c) `800 + 2` of type `Nat`
+  **a)** `fun x => x` of type `Bool → Bool`  
+  **b)** `(fun x => x) ((true && false) || true)` of type `Bool`  
+  **c)** `800 + 2` of type `Nat`
 7. [**Computation**] Show that `1` created with `Expr.lit (Lean.Literal.natVal 1)` is definitionally equal to an expression created with `Expr.app (Expr.const ``Nat.succ []) (Expr.const ``Nat.zero [])`.
 8. [**Computation**] Determine whether the following expressions are definitionally equal. If `Lean.Meta.isDefEq` succeeds, and it leads to metavariable assignment, write down the assignments.  
-  a) `5 =?= (λ x => 5) ((λ y : Nat → Nat => y) (λ z : Nat => z))`  
-  b) `2 + 1 =?= 1 + 2`  
-  c) `?a =?= 2`, where `?a` has a type `String`  
-  d) `?a + Int =?= "hi" + ?b`, where `?a` and `?b` don't have a type  
-  e) `2 + ?a =?= 3`  
-  f) `2 + ?a =?= 2 + 1`
+  **a)** `5 =?= (fun x => 5) ((fun y : Nat → Nat => y) (fun z : Nat => z))`  
+  **b)** `2 + 1 =?= 1 + 2`  
+  **c)** `?a =?= 2`, where `?a` has a type `String`  
+  **d)** `?a + Int =?= "hi" + ?b`, where `?a` and `?b` don't have a type  
+  **e)** `2 + ?a =?= 3`  
+  **f)** `2 + ?a =?= 2 + 1`
 9. [**Computation**] Write down what you expect the following code to output.
 
 ```
@@ -1262,16 +1300,16 @@ def defaultDef                    : Nat := 3
   let reducedExpr ← Meta.reduce constantExpr
   dbg_trace (← ppExpr reducedExpr) -- ...
 ```
-10. [**Constructing Expressions**] Create expression `λ x, 1 + x` in two ways:  
-  a) not idiomatically, with loose bound variables  
-  b) idiomatically.  
+10. [**Constructing Expressions**] Create expression `fun x, 1 + x` in two ways:  
+  **a)** not idiomatically, with loose bound variables  
+  **b)** idiomatically.  
   In what version can you use `Lean.mkAppN`? In what version can you use `Lean.Meta.mkAppM`?
 11. [**Constructing Expressions**] Create expression `∀ (yellow: Nat), yellow`.
 12. [**Constructing Expressions**] Create expression `∀ (n : Nat), n = n + 1` in two ways:  
-  a) not idiomatically, with loose bound variables  
-  b) idiomatically.  
+  **a)** not idiomatically, with loose bound variables  
+  **b)** idiomatically.  
   In what version can you use `Lean.mkApp3`? In what version can you use `Lean.Meta.mkEq`?
-13. [**Constructing Expressions**] Create expression `λ (f : Nat → Nat), ∀ (n : Nat), f n = f (n + 1)` idiomatically.
+13. [**Constructing Expressions**] Create expression `fun (f : Nat → Nat), ∀ (n : Nat), f n = f (n + 1)` idiomatically.
 14. [**Constructing Expressions**] What would you expect the output of the following code to be?
 
 ```
diff --git a/lean/main/syntax.lean b/lean/main/syntax.lean
index 9be62a5..5b9e6f6 100644
--- a/lean/main/syntax.lean
+++ b/lean/main/syntax.lean
@@ -220,10 +220,12 @@ syntax "[Bool|" boolean_expr "]" : term
 ### Syntax combinators
 In order to declare more complex syntax, it is often very desirable to have
 some basic operations on syntax already built-in, these include:
+
 - helper parsers without syntax categories (i.e. not extendable)
 - alternatives
 - repetitive parts
 - optional parts
+
 While all of these do have an encoding based on syntax categories, this
 can make things quite ugly at times, so Lean provides an easier way to do all
 of these.
@@ -551,4 +553,74 @@ it in the way we would expect it.
 As to how one might extend this notation to allow more set-theoretic
 things such as `{x ∈ X | p x}` and leave out the parentheses around
 the bound variables, we refer the reader to the macro chapter.
+
+
+## Exercises
+
+1. Create an "urgent minus 💀" notation such that `5 * 8 💀 4` returns `20`, and `8 💀 6 💀 1` returns `3`.
+
+**a)** Using `notation` command.  
+**b)** Using `infix` command.  
+**c)** Using `syntax` command.  
+
+Hint: multiplication in Lean 4 is defined as `infixl:70 " * " => HMul.hMul`.
+
+2. Consider the following syntax categories: `term`, `command`, `tactic`; and 3 syntax rules given below. Make use of each of these newly defined syntaxes.
+
+```
+  syntax "good morning" : term
+  syntax "hello" : command
+  syntax "yellow" : tactic
+```
+
+3. Create a `syntax` rule that would accept the following commands:
+
+- `red red red 4`
+- `blue 7`
+- `blue blue blue blue blue 18`
+
+(So, either all `red`s followed by a number; or all `blue`s followed by a number; `red blue blue 5` - shouldn't work.)
+
+Use the following code template:
+
+```
+syntax (name := colors) ...
+-- our "elaboration function" that infuses syntax with semantics
+@[command_elab colors] def elabColors : CommandElab := λ stx => Lean.logInfo "success!"
+```
+
+4. Mathlib has a `#help option` command that displays all options available in the current environment, and their descriptions. `#help option pp.r` will display all options starting with a "pp.r" substring.
+
+Create a `syntax` rule that would accept the following commands:
+
+- `#better_help option`
+- `#better_help option pp.r`
+- `#better_help option some.other.name`
+
+Use the following template:
+
+```
+syntax (name := help) ...
+-- our "elaboration function" that infuses syntax with semantics
+@[command_elab help] def elabHelp : CommandElab := λ stx => Lean.logInfo "success!"
+```
+
+5. Mathlib has a ∑ operator. Create a `syntax` rule that would accept the following terms:
+
+- `∑ x in { 1, 2, 3 }, x^2`
+- `∑ x in { "apple", "banana", "cherry" }, x.length`
+
+Use the following template:
+
+```
+import Std.Classes.SetNotation
+import Std.Util.ExtendedBinder
+syntax (name := bigsumin) ...
+-- our "elaboration function" that infuses syntax with semantics
+@[term_elab bigsumin] def elabSum : TermElab := λ stx tp => return mkNatLit 666
+```
+
+Hint: use the `Std.ExtendedBinder.extBinder` parser.
+Hint: you need Std4 installed in your Lean project for these imports to work.
+
 -/
diff --git a/lean/solutions/elaboration.lean b/lean/solutions/elaboration.lean
new file mode 100644
index 0000000..d90efed
--- /dev/null
+++ b/lean/solutions/elaboration.lean
@@ -0,0 +1,90 @@
+import Lean
+open Lean Elab Command Term Meta
+
+/- ## Elaboration: Solutions -/
+
+/- ### 1. -/
+
+elab n:term "♥" a:"♥"? b:"♥"? : term => do
+  let nExpr : Expr ← elabTermEnsuringType n (mkConst `Nat)
+  if let some a := a then
+    if let some b := b then
+      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 3)
+    else
+      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 2)
+  else
+    return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 1)
+
+#eval 7 ♥ -- 8
+#eval 7 ♥♥ -- 9
+#eval 7 ♥♥♥ -- 10
+
+/- ### 2. -/
+
+-- a) using `syntax` + `@[command_elab alias] def elabOurAlias : CommandElab`
+syntax (name := aliasA) (docComment)? "aliasA " ident " ← " ident* : command
+
+@[command_elab «aliasA»]
+def elabOurAlias : CommandElab := λ stx =>
+  match stx with
+  | `(aliasA $x:ident ← $ys:ident*) =>
+    for y in ys do
+      Lean.logInfo y
+  | _ =>
+    throwUnsupportedSyntax
+
+aliasA hi.hello ← d.d w.w nnn
+
+-- b) using `syntax` + `elab_rules`.
+syntax (name := aliasB) (docComment)? "aliasB " ident " ← " ident* : command
+
+elab_rules : command
+  | `(command | aliasB $m:ident ← $ys:ident*) =>
+    for y in ys do
+      Lean.logInfo y
+
+aliasB hi.hello ← d.d w.w nnn
+
+-- c) using `elab`
+elab "aliasC " x:ident " ← " ys:ident* : command =>
+  for y in ys do
+    Lean.logInfo y
+
+aliasC hi.hello ← d.d w.w nnn
+
+/- ### 3. -/
+
+open Parser.Tactic
+
+-- a) using `syntax` + `@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic`.
+syntax (name := nthRewriteA) "nth_rewriteA " (config)? num rwRuleSeq (ppSpace location)? : tactic
+
+@[tactic nthRewriteA] def elabNthRewrite : Lean.Elab.Tactic.Tactic := fun stx => do
+  match stx with
+  | `(tactic| nth_rewriteA $[$cfg]? $n $rules $_loc) =>
+    Lean.logInfo "rewrite location!"
+  | `(tactic| nth_rewriteA $[$cfg]? $n $rules) =>
+    Lean.logInfo "rewrite target!"
+  | _ =>
+    throwUnsupportedSyntax
+
+-- b) using `syntax` + `elab_rules`.
+syntax (name := nthRewriteB) "nth_rewriteB " (config)? num rwRuleSeq (ppSpace location)? : tactic
+
+elab_rules (kind := nthRewriteB) : tactic
+  | `(tactic| nth_rewriteB $[$cfg]? $n $rules $_loc) =>
+    Lean.logInfo "rewrite location!"
+  | `(tactic| nth_rewriteB $[$cfg]? $n $rules) =>
+    Lean.logInfo "rewrite target!"
+
+-- c) using `elab`.
+elab "nth_rewriteC " (config)? num rwRuleSeq loc:(ppSpace location)? : tactic =>
+  if let some loc := loc then
+    Lean.logInfo "rewrite location!"
+  else
+    Lean.logInfo "rewrite target!"
+
+example : 2 + 2 = 4 := by
+  nth_rewriteC 2 [← add_zero] at h
+  nth_rewriteC 2 [← add_zero]
+  sorry
diff --git a/lean/solutions/expressions.lean b/lean/solutions/expressions.lean
index a51aab0..682bb4f 100644
--- a/lean/solutions/expressions.lean
+++ b/lean/solutions/expressions.lean
@@ -4,7 +4,7 @@ open Lean Meta
 /- # Solutions -/
 /- ## Expressions: Solutions -/
 
-/- 1. Create expression `1 + 2` with `Expr.app`. -/
+/- ### 1. -/
 def one : Expr :=
   Expr.app (Expr.app (Expr.const `Nat.add []) (mkNatLit 1)) (mkNatLit 2)
 
@@ -12,7 +12,7 @@ elab "one" : term => return one
 #check one  -- Nat.add 1 2 : Nat
 #reduce one -- 3
 
-/- 2. Create expression `1 + 2` with `Lean.mkAppN`. -/
+/- ### 2. -/
 def two : Expr :=
   Lean.mkAppN (Expr.const `Nat.add []) #[mkNatLit 1, mkNatLit 2]
 
@@ -20,7 +20,7 @@ elab "two" : term => return two
 #check two  -- Nat.add 1 2 : Nat
 #reduce two -- 3
 
-/- 3. Create expression `λ x => 1 + x`. -/
+/- ### 3. -/
 def three : Expr :=
   Expr.lam `x (Expr.const `Nat [])
   (Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkNatLit 1, Expr.bvar 0])
@@ -30,7 +30,7 @@ elab "three" : term => return three
 #check three    -- fun x => Nat.add 1 x : Nat → Nat
 #reduce three 6 -- 7
 
-/- 4. [**De Bruijn Indexes**] Create expression `λ a, λ b, λ c, (b * a) + c`. -/
+/- ### 4. -/
 def four : Expr :=
   Expr.lam `a (Expr.const `Nat [])
   (
@@ -55,7 +55,7 @@ elab "four" : term => return four
 #check four -- fun a b c => Nat.add (Nat.mul b a) c : Nat → Nat → Nat → Nat
 #reduce four 666 1 2 -- 668
 
-/- 5. Create expression `λ x y => x + y`. -/
+/- ### 5. -/
 def five :=
   Expr.lam `x (Expr.const `Nat [])
   (
@@ -69,7 +69,7 @@ elab "five" : term => return five
 #check five      -- fun x y => Nat.add x y : Nat → Nat → Nat
 #reduce five 4 5 -- 9
 
-/- 6. Create expression `λ x, String.append "hello, " x`. -/
+/- ### 6. -/
 def six :=
   Expr.lam `x (Expr.const `String [])
   (Lean.mkAppN (Expr.const `String.append []) #[Lean.mkStrLit "Hello, ", Expr.bvar 0])
@@ -79,7 +79,7 @@ elab "six" : term => return six
 #check six        -- fun x => String.append "Hello, " x : String → String
 #eval six "world" -- "Hello, world"
 
-/- 7. Create expression `∀ x : Prop, x ∧ x`. -/
+/- ### 7. -/
 def seven : Expr :=
   Expr.forallE `x (Expr.sort Lean.Level.zero)
   (Expr.app (Expr.app (Expr.const `And []) (Expr.bvar 0)) (Expr.bvar 0))
@@ -89,7 +89,7 @@ elab "seven" : term => return seven
 #check seven  -- ∀ (x : Prop), x ∧ x : Prop
 #reduce seven -- ∀ (x : Prop), x ∧ x
 
-/- 8. Create expression `Nat → String`. -/
+/- ### 8. -/
 def eight : Expr :=
   Expr.forallE `notUsed
   (Expr.const `Nat []) (Expr.const `String [])
@@ -99,7 +99,7 @@ elab "eight" : term => return eight
 #check eight  -- Nat → String : Type
 #reduce eight -- Nat → String
 
-/- 9. Create expression `λ (p : Prop) => (λ hP : p => hP)`. -/
+/- ### 9. -/
 def nine : Expr :=
   Expr.lam `p (Expr.sort Lean.Level.zero)
   (
@@ -113,7 +113,7 @@ elab "nine" : term => return nine
 #check nine  -- fun p hP => hP : ∀ (p : Prop), p → p
 #reduce nine -- fun p hP => hP
 
-/- 10. [**Universe levels**] Create expression `Type 6`. -/
+/- ### 10. -/
 def ten : Expr :=
   Expr.sort (Nat.toLevel 7)
 
diff --git a/lean/solutions/metam.lean b/lean/solutions/metam.lean
index de51228..de63495 100644
--- a/lean/solutions/metam.lean
+++ b/lean/solutions/metam.lean
@@ -3,8 +3,7 @@ open Lean Meta
 
 /- ## `MetaM`: Solutions -/
 
-/- 1. [**Metavariables**] Create a metavariable with type `Nat`, and assign to it value `3`.
-Notice that changing the type of the metavarible from `Nat` to, for example, `String`, doesn't raise any errors - that's why, as was mentioned, we must make sure *"(a) that `val` must have the target type of `mvarId` and (b) that `val` must only contain `fvars` from the local context of `mvarId`".* -/
+/- ### 1. -/
 
 #eval show MetaM Unit from do
   let hi ← Lean.Meta.mkFreshExprMVar (Expr.const `Nat []) (userName := `hi)
@@ -13,14 +12,14 @@ Notice that changing the type of the metavarible from `Nat` to, for example, `St
   hi.mvarId!.assign (Expr.app (Expr.const `Nat.succ []) (Expr.const ``Nat.zero []))
   IO.println s!"value in hi: {← instantiateMVars hi}" -- Nat.succ Nat.zero
 
-/- 2. [**Metavariables**] What would `instantiateMVars (Lean.mkAppN (Expr.const 'Nat.add []) #[mkNatLit 1, mkNatLit 2])` output? -/
+/- ### 2. -/
 
 -- It would output the same expression we gave it - there were no metavariables to instantiate.
 #eval show MetaM Unit from do
   let instantiatedExpr ← instantiateMVars (Expr.lam `x (Expr.const `Nat []) (Expr.bvar 0) BinderInfo.default)
   IO.println instantiatedExpr -- fun (x : Nat) => x
 
-/- 3. [**Metavariables**] Fill in the missing lines in the following code. ... -/
+/- ### 3. -/
 
 #eval show MetaM Unit from do
   let oneExpr := Expr.app (Expr.const `Nat.succ []) (Expr.const ``Nat.zero [])
@@ -43,11 +42,7 @@ Notice that changing the type of the metavarible from `Nat` to, for example, `St
   let instantiatedMvar1 ← instantiateMVars mvar1
   IO.println instantiatedMvar1 -- Nat.add (Nat.add 2 ?_uniq.2) 1
 
-/- 4. [**Metavariables**] Consider the theorem `red`, and tactic `explore` below.  
-a) What would be the `type` and `userName` of metavariable `mvarId`?  
-b) What would be the `type`s and `userName`s of all local declarations in this metavariable's local context?  
-Print them all out. ...
--/
+/- ### 4. -/
 
 elab "explore" : tactic => do
   let mvarId : MVarId ← Lean.Elab.Tactic.getMainGoal
@@ -72,7 +67,7 @@ theorem red (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by
   explore
   sorry
 
-/- 5. [**Metavariables**] Write a tactic `solve` that proves the theorem `red`. -/
+/- ### 5. -/
 
 -- The type of our metavariable `2 + 2`. We want to find a `localDecl` that has the same type, and `assign` our metavariable to that `localDecl`.
 elab "solve" : tactic => do
@@ -87,18 +82,13 @@ elab "solve" : tactic => do
 theorem redSolved (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by
   solve
 
+/- ### 6. -/
 
-/- 6. [**Computation**] What is the normal form of the following expressions:  
-a) `λ x => x` of type `Bool → Bool`  
-b) `(λ x => x) ((true && false) || true)` of type `Bool`  
-c) `800 + 2` of type `Nat`
--/
-
-def sixA : Bool → Bool := λ x => x
+def sixA : Bool → Bool := fun x => x
 -- .lam `x (.const `Bool []) (.bvar 0) (Lean.BinderInfo.default)
 #eval Lean.Meta.reduce (Expr.const `sixA [])
 
-def sixB : Bool := (λ x => x) ((true && false) || true)
+def sixB : Bool := (fun x => x) ((true && false) || true)
 -- .const `Bool.true []
 #eval Lean.Meta.reduce (Expr.const `sixB [])
 
@@ -106,7 +96,8 @@ def sixC : Nat := 800 + 2
 -- .lit (Lean.Literal.natVal 802)
 #eval Lean.Meta.reduce (Expr.const `sixC [])
 
-/- 7. [**Computation**] Show that `1` created with `Expr.lit (Lean.Literal.natVal 1)` is definitionally equal to an expression created with `Expr.app (Expr.const ``Nat.succ []) (Expr.const ``Nat.zero [])`. -/
+/- ### 7. -/
+
 #eval show MetaM Unit from do
   let litExpr := Expr.lit (Lean.Literal.natVal 1)
   let standardExpr := Expr.app (Expr.const ``Nat.succ []) (Expr.const ``Nat.zero [])
@@ -114,18 +105,11 @@ def sixC : Nat := 800 + 2
   let isEqual ← Lean.Meta.isDefEq litExpr standardExpr
   IO.println isEqual -- true
 
-/- 8. [**Computation**] Determine whether the following expressions are definitionally equal. If `Lean.Meta.isDefEq` succeeds, and it leads to metavariable assignment, write down the assignments.  
-a) `5 =?= (λ x => 5) ((λ y : Nat → Nat => y) (λ z : Nat => z))`  
-b) `2 + 1 =?= 1 + 2`  
-c) `?a =?= 2`, where `?a` has a type `String`  
-d) `?a + Int =?= "hi" + ?b`, where `?a` and `?b` don't have a type  
-e) `2 + ?a =?= 3`  
-f) `2 + ?a =?= 2 + 1`
--/
+/- ### 8. -/
 
--- a) `5 =?= (λ x => 5) ((λ y : Nat → Nat => y) (λ z : Nat => z))`
+-- a) `5 =?= (fun x => 5) ((fun y : Nat → Nat => y) (fun z : Nat => z))`
 -- Definitionally equal.
-def expr2 := (λ x => 5) ((λ y : Nat → Nat => y) (λ z : Nat => z))
+def expr2 := (fun x => 5) ((fun y : Nat → Nat => y) (fun z : Nat => z))
 #eval show MetaM Unit from do
   let expr1 := Lean.mkNatLit 5
   let expr2 := Expr.const `expr2 []
@@ -183,7 +167,7 @@ def expr2 := (λ x => 5) ((λ y : Nat → Nat => y) (λ z : Nat => z))
 
   IO.println s!"a: {← instantiateMVars a}"
 
-/- 9. [**Computation**] Write down what you expect the following code to output. ...-/
+/- ### 9. -/
 @[reducible] def reducibleDef     : Nat := 1 -- same as `abbrev`
 @[instance] def instanceDef       : Nat := 2 -- same as `instance`
 def defaultDef                    : Nat := 3
@@ -214,11 +198,7 @@ def defaultDef                    : Nat := 3
   let reducedExpr ← Meta.reduce constantExpr
   dbg_trace (← ppExpr reducedExpr) -- [1, 2, 3, irreducibleDef]
 
-/- 10. [**Constructing Expressions**] Create expression `λ x, 1 + x` in two ways:  
-a) not idiomatically, with loose bound variables  
-b) idiomatically.  
-In what version can you use `Lean.mkAppN`? In what version can you use `Lean.Meta.mkAppM`?
--/
+/- ### 10. -/
 
 -- Non-idiomatic: we can only use `Lean.mkAppN`.
 def tenA : MetaM Expr := do
@@ -227,7 +207,7 @@ def tenA : MetaM Expr := do
 
 -- Idiomatic: we can use both `Lean.mkAppN` and `Lean.Meta.mkAppM`.
 def tenB : MetaM Expr := do
-  Lean.Meta.withLocalDecl `x .default (Expr.const `Nat []) (λ x => do
+  Lean.Meta.withLocalDecl `x .default (Expr.const `Nat []) (fun x => do
     -- let body := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkNatLit 1, x]
     let body ← Lean.Meta.mkAppM `Nat.add #[Lean.mkNatLit 1, x]
     Lean.Meta.mkLambdaFVars #[x] body
@@ -238,7 +218,7 @@ def tenB : MetaM Expr := do
 #eval show MetaM _ from do
   ppExpr (← tenB) -- fun x => Nat.add 1 x
 
-/- 11. [**Constructing Expressions**] Create expression `∀ (yellow: Nat), yellow`. -/
+/- ### 11. -/
 
 def eleven : MetaM Expr :=
   return Expr.forallE `yellow (Expr.const `Nat []) (Expr.bvar 0) BinderInfo.default
@@ -246,11 +226,7 @@ def eleven : MetaM Expr :=
 #eval show MetaM _ from do
   dbg_trace (← eleven) -- forall (yellow : Nat), yellow
 
-/- 12. [**Constructing Expressions**] Create expression `∀ (n : Nat), n = n + 1` in two ways:  
-a) not idiomatically, with loose bound variables  
-b) idiomatically.  
-In what version can you use `Lean.mkApp3`? In what version can you use `Lean.Meta.mkEq`?
--/
+/- ### 12. -/
 
 -- Non-idiomatic: we can only use `Lean.mkApp3`.
 def twelveA : MetaM Expr := do
@@ -261,7 +237,7 @@ def twelveA : MetaM Expr := do
 
 -- Idiomatic: we can use both `Lean.mkApp3` and `Lean.Meta.mkEq`.
 def twelveB : MetaM Expr := do
-  withLocalDecl `n BinderInfo.default (Expr.const `Nat []) (λ x => do
+  withLocalDecl `n BinderInfo.default (Expr.const `Nat []) (fun x => do
     let nPlusOne := Expr.app (Expr.app (Expr.const `Nat.add []) x) (Lean.mkNatLit 1)
     -- let forAllBody := Lean.mkApp3 (Expr.const ``Eq []) (Expr.const `Nat []) x nPlusOne
     let forAllBody ← Lean.Meta.mkEq x nPlusOne
@@ -275,10 +251,10 @@ def twelveB : MetaM Expr := do
 #eval show MetaM _ from do
   ppExpr (← twelveB) -- ∀ (n : Nat), n = Nat.add n 1
 
-/- 13. [**Constructing Expressions**] Create expression `λ (f : Nat → Nat), ∀ (n : Nat), f n = f (n + 1)` idiomatically. -/
+/- ### 13. -/
 def thirteen : MetaM Expr := do
-  withLocalDecl `f BinderInfo.default (Expr.forallE `a (Expr.const `Nat []) (Expr.const `Nat []) .default) (λ y => do
-    let lamBody ← withLocalDecl `n BinderInfo.default (Expr.const `Nat []) (λ x => do
+  withLocalDecl `f BinderInfo.default (Expr.forallE `a (Expr.const `Nat []) (Expr.const `Nat []) .default) (fun y => do
+    let lamBody ← withLocalDecl `n BinderInfo.default (Expr.const `Nat []) (fun x => do
       let fn := Expr.app y x
       let fnPlusOne := Expr.app y (Expr.app (Expr.app (Expr.const `Nat.add []) (x)) (Lean.mkNatLit 1))
       let forAllBody := mkApp3 (mkConst ``Eq []) (Expr.const `Nat []) fn fnPlusOne
@@ -292,7 +268,7 @@ def thirteen : MetaM Expr := do
 #eval show MetaM _ from do
   ppExpr (← thirteen) -- fun f => (n : Nat) → Eq Nat (f n) (f (Nat.add n 1))
 
-/- 14. [**Constructing Expressions**] What would you expect the output of the following code to be?... -/
+/- ### 14. -/
 
 #eval show Lean.Elab.Term.TermElabM _ from do
   let stx : Syntax ← `(∀ (a : Prop) (b : Prop), a ∨ b → b → a ∧ a)
@@ -307,8 +283,7 @@ def thirteen : MetaM Expr := do
   let (_, _, conclusion) ← lambdaMetaTelescope expr
   dbg_trace conclusion -- forall (a.1 : Prop) (b.1 : Prop), (Or a.1 b.1) -> b.1 -> (And a.1 a.1)
 
-/- 15. [**Backtracking**] Check that the expressions `?a + Int` and `"hi" + ?b` are definitionally equal with `isDefEq` (make sure to use the proper types or `Option.none` for the types of your metavariables!).
-Use `saveState` and `restoreState` to revert metavariable assignments. -/
+/- ### 15. -/
 
 #eval show MetaM Unit from do
   let a ← Lean.Meta.mkFreshExprMVar (Expr.const `String []) (userName := `a)
diff --git a/lean/solutions/syntax.lean b/lean/solutions/syntax.lean
new file mode 100644
index 0000000..8443ceb
--- /dev/null
+++ b/lean/solutions/syntax.lean
@@ -0,0 +1,80 @@
+import Lean
+import Lean.Parser.Syntax
+
+open Lean Elab Command Term
+
+/- ## `Syntax`: Solutions -/
+
+/- ### 1. -/
+
+namespace a
+  scoped notation:71 lhs:50 " 💀 " rhs:72 => lhs - rhs
+end a
+
+namespace b
+  set_option quotPrecheck false
+  scoped infixl:71 " 💀 " => fun lhs rhs => lhs - rhs
+end b
+
+namespace c
+  scoped syntax:71 term:50 " 💀 " term:72 : term
+  scoped macro_rules | `($l:term 💀 $r:term) => `($l - $r)
+end c
+
+open a
+#eval 5 * 8 💀 4 -- 20
+#eval 8 💀 6 💀 1 -- 1
+
+/- ### 2. -/
+
+syntax "good morning" : term
+syntax "hello" : command
+syntax "yellow" : tactic
+
+-- Note: the following are highlighted in red, however that's just because we haven't implemented the semantics ("elaboration function") yet - the syntax parsing stage works.
+
+#eval good morning -- works
+-- good morning -- error: `expected command`
+
+hello -- works
+-- #eval hello -- error: `expected term`
+
+example : 2 + 2 = 4 := by
+  yellow -- works
+-- yellow -- error: `expected command`
+-- #eval yellow -- error: `unknown identifier 'yellow'`
+
+/- ### 3. -/
+
+syntax (name := colors) (("blue"+) <|> ("red"+)) num : command
+
+@[command_elab colors]
+def elabColors : CommandElab := fun stx => Lean.logInfo "success!"
+
+blue blue 443
+red red red 4
+
+/- ### 4. -/
+
+syntax (name := help) "#better_help" "option" (ident)? : command
+
+@[command_elab help]
+def elabHelp : CommandElab := fun stx => Lean.logInfo "success!"
+
+#better_help option
+#better_help option pp.r
+#better_help option some.other.name
+
+/- ### 5. -/
+
+-- Note: std4 has to be in dependencies of your project for this to work.
+syntax (name := bigsumin) "∑ " Std.ExtendedBinder.extBinder "in " term "," term : term
+
+@[term_elab bigsumin]
+def elabSum : TermElab := fun stx tp =>
+  return mkNatLit 666
+
+#eval ∑ x in { 1, 2, 3 }, x^2
+
+def hi := (∑ x in { "apple", "banana", "cherry" }, x.length) + 1
+#eval hi
diff --git a/md/main/elaboration.md b/md/main/elaboration.md
index 7f23022..ebb55d9 100644
--- a/md/main/elaboration.md
+++ b/md/main/elaboration.md
@@ -342,3 +342,55 @@ syntax sugar of the `elab` syntax instead:
 elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do 
   sorry
 ```
+
+## Exercises
+
+1. Consider the following code. Rewrite `syntax` + `@[term_elab hi]... : TermElab` combination using just `elab`.
+
+```
+syntax (name := hi) term " ♥ " " ♥ "? " ♥ "? : term
+
+@[term_elab hi]
+def heartElab : TermElab := fun stx tp =>
+  match stx with
+    | `($l:term ♥) => do
+      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
+      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 1)
+    | `($l:term ♥♥) => do
+      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
+      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 2)
+    | `($l:term ♥♥♥) => do
+      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
+      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 3)
+    | _ =>
+      throwUnsupportedSyntax
+```
+
+2. Here is some syntax taken from a real mathlib command `alias`.
+
+```
+syntax (name := our_alias) (docComment)? "our_alias " ident " ← " ident* : command
+```
+
+We want `alias hi ← hello yes` to print out the identifiers after `←` - that is, "hello" and "yes".
+
+Please add these semantics:
+
+**a)** using `syntax` + `@[command_elab alias] def elabOurAlias : CommandElab`.  
+**b)** using `syntax` + `elab_rules`.  
+**c)** using `elab`.
+
+3. Here is some syntax taken from a real mathlib tactic `nth_rewrite`.
+
+```
+open Parser.Tactic
+syntax (name := nthRewriteSeq) "nth_rewrite " (config)? num rwRuleSeq (ppSpace location)? : tactic
+```
+
+We want `nth_rewrite 5 [←add_zero a] at h` to print out `"rewrite location!"` if the user provided location, and `"rewrite target!"` if the user didn't provide location.
+
+Please add these semantics:
+
+**a)** using `syntax` + `@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic`.  
+**b)** using `syntax` + `elab_rules`.  
+**c)** using `elab`.
diff --git a/md/main/expressions.md b/md/main/expressions.md
index 6a23c42..2fc7c77 100644
--- a/md/main/expressions.md
+++ b/md/main/expressions.md
@@ -272,11 +272,11 @@ expressions.
 
 1. Create expression `1 + 2` with `Expr.app`.
 2. Create expression `1 + 2` with `Lean.mkAppN`.
-3. Create expression `λ x => 1 + x`.
-4. [**De Bruijn Indexes**] Create expression `λ a, λ b, λ c, (b * a) + c`.
-5. Create expression `λ x y => x + y`.
-6. Create expression `λ x, String.append "hello, " x`.
+3. Create expression `fun x => 1 + x`.
+4. [**De Bruijn Indexes**] Create expression `fun a, fun b, fun c, (b * a) + c`.
+5. Create expression `fun x y => x + y`.
+6. Create expression `fun x, String.append "hello, " x`.
 7. Create expression `∀ x : Prop, x ∧ x`.
 8. Create expression `Nat → String`.
-9. Create expression `λ (p : Prop) => (λ hP : p => hP)`.
+9. Create expression `fun (p : Prop) => (λ hP : p => hP)`.
 10. [**Universe levels**] Create expression `Type 6`.
diff --git a/md/main/metam.md b/md/main/metam.md
index 3f26f60..6a148fb 100644
--- a/md/main/metam.md
+++ b/md/main/metam.md
@@ -1211,23 +1211,61 @@ Lean parser.
 Notice that changing the type of the metavarible from `Nat` to, for example, `String`, doesn't raise any errors - that's why, as was mentioned, we must make sure *"(a) that `val` must have the target type of `mvarId` and (b) that `val` must only contain `fvars` from the local context of `mvarId`"*.
 2. [**Metavariables**] What would `instantiateMVars (Lean.mkAppN (Expr.const 'Nat.add []) #[mkNatLit 1, mkNatLit 2])` output?
 3. [**Metavariables**] Fill in the missing lines in the following code.
+
+  ```
+  #eval show MetaM Unit from do
+    let oneExpr := Expr.app (Expr.const `Nat.succ []) (Expr.const ``Nat.zero [])
+    let twoExpr := Expr.app (Expr.const `Nat.succ []) oneExpr
+
+    -- Create `mvar1` with type `Nat`
+    -- let mvar1 ← ...
+    -- Create `mvar2` with type `Nat`
+    -- let mvar2 ← ...
+    -- Create `mvar3` with type `Nat`
+    -- let mvar3 ← ...
+
+    -- Assign `mvar1` to `2 + ?mvar2 + ?mvar3`
+    -- ...
+
+    -- Assign `mvar3` to `1`
+    -- ...
+
+    -- Instantiate `mvar1`, which should result in expression `2 + ?mvar2 + 1`
+    ...
+  ```
 4. [**Metavariables**] Consider the theorem `red`, and tactic `explore` below.  
   a) What would be the `type` and `userName` of metavariable `mvarId`?  
   b) What would be the `type`s and `userName`s of all local declarations in this metavariable's local context?  
   Print them all out.
+
+  ```
+  elab "explore" : tactic => do
+    let mvarId : MVarId ← Lean.Elab.Tactic.getMainGoal
+    let metavarDecl : MetavarDecl ← mvarId.getDecl
+
+    IO.println "Our metavariable"
+    -- ...
+
+    IO.println "All of its local declarations"
+    -- ...
+
+  theorem red (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by
+    explore
+    sorry
+  ```
 5. [**Metavariables**] Write a tactic `solve` that proves the theorem `red`.
 6. [**Computation**] What is the normal form of the following expressions:  
-  a) `λ x => x` of type `Bool → Bool`  
-  b) `(λ x => x) ((true && false) || true)` of type `Bool`  
-  c) `800 + 2` of type `Nat`
+  **a)** `fun x => x` of type `Bool → Bool`  
+  **b)** `(fun x => x) ((true && false) || true)` of type `Bool`  
+  **c)** `800 + 2` of type `Nat`
 7. [**Computation**] Show that `1` created with `Expr.lit (Lean.Literal.natVal 1)` is definitionally equal to an expression created with `Expr.app (Expr.const ``Nat.succ []) (Expr.const ``Nat.zero [])`.
 8. [**Computation**] Determine whether the following expressions are definitionally equal. If `Lean.Meta.isDefEq` succeeds, and it leads to metavariable assignment, write down the assignments.  
-  a) `5 =?= (λ x => 5) ((λ y : Nat → Nat => y) (λ z : Nat => z))`  
-  b) `2 + 1 =?= 1 + 2`  
-  c) `?a =?= 2`, where `?a` has a type `String`  
-  d) `?a + Int =?= "hi" + ?b`, where `?a` and `?b` don't have a type  
-  e) `2 + ?a =?= 3`  
-  f) `2 + ?a =?= 2 + 1`
+  **a)** `5 =?= (fun x => 5) ((fun y : Nat → Nat => y) (fun z : Nat => z))`  
+  **b)** `2 + 1 =?= 1 + 2`  
+  **c)** `?a =?= 2`, where `?a` has a type `String`  
+  **d)** `?a + Int =?= "hi" + ?b`, where `?a` and `?b` don't have a type  
+  **e)** `2 + ?a =?= 3`  
+  **f)** `2 + ?a =?= 2 + 1`
 9. [**Computation**] Write down what you expect the following code to output.
 
 ```
@@ -1260,16 +1298,16 @@ def defaultDef                    : Nat := 3
   let reducedExpr ← Meta.reduce constantExpr
   dbg_trace (← ppExpr reducedExpr) -- ...
 ```
-10. [**Constructing Expressions**] Create expression `λ x, 1 + x` in two ways:  
-  a) not idiomatically, with loose bound variables  
-  b) idiomatically.  
+10. [**Constructing Expressions**] Create expression `fun x, 1 + x` in two ways:  
+  **a)** not idiomatically, with loose bound variables  
+  **b)** idiomatically.  
   In what version can you use `Lean.mkAppN`? In what version can you use `Lean.Meta.mkAppM`?
 11. [**Constructing Expressions**] Create expression `∀ (yellow: Nat), yellow`.
 12. [**Constructing Expressions**] Create expression `∀ (n : Nat), n = n + 1` in two ways:  
-  a) not idiomatically, with loose bound variables  
-  b) idiomatically.  
+  **a)** not idiomatically, with loose bound variables  
+  **b)** idiomatically.  
   In what version can you use `Lean.mkApp3`? In what version can you use `Lean.Meta.mkEq`?
-13. [**Constructing Expressions**] Create expression `λ (f : Nat → Nat), ∀ (n : Nat), f n = f (n + 1)` idiomatically.
+13. [**Constructing Expressions**] Create expression `fun (f : Nat → Nat), ∀ (n : Nat), f n = f (n + 1)` idiomatically.
 14. [**Constructing Expressions**] What would you expect the output of the following code to be?
 
 ```
diff --git a/md/main/syntax.md b/md/main/syntax.md
index 0a0d792..40c9887 100644
--- a/md/main/syntax.md
+++ b/md/main/syntax.md
@@ -219,10 +219,12 @@ syntax "[Bool|" boolean_expr "]" : term
 ### Syntax combinators
 In order to declare more complex syntax, it is often very desirable to have
 some basic operations on syntax already built-in, these include:
+
 - helper parsers without syntax categories (i.e. not extendable)
 - alternatives
 - repetitive parts
 - optional parts
+
 While all of these do have an encoding based on syntax categories, this
 can make things quite ugly at times, so Lean provides an easier way to do all
 of these.
@@ -549,3 +551,72 @@ it in the way we would expect it.
 As to how one might extend this notation to allow more set-theoretic
 things such as `{x ∈ X | p x}` and leave out the parentheses around
 the bound variables, we refer the reader to the macro chapter.
+
+
+## Exercises
+
+1. Create an "urgent minus 💀" notation such that `5 * 8 💀 4` returns `20`, and `8 💀 6 💀 1` returns `3`.
+
+**a)** Using `notation` command.  
+**b)** Using `infix` command.  
+**c)** Using `syntax` command.  
+
+Hint: multiplication in Lean 4 is defined as `infixl:70 " * " => HMul.hMul`.
+
+2. Consider the following syntax categories: `term`, `command`, `tactic`; and 3 syntax rules given below. Make use of each of these newly defined syntaxes.
+
+```
+  syntax "good morning" : term
+  syntax "hello" : command
+  syntax "yellow" : tactic
+```
+
+3. Create a `syntax` rule that would accept the following commands:
+
+- `red red red 4`
+- `blue 7`
+- `blue blue blue blue blue 18`
+
+(So, either all `red`s followed by a number; or all `blue`s followed by a number; `red blue blue 5` - shouldn't work.)
+
+Use the following code template:
+
+```
+syntax (name := colors) ...
+-- our "elaboration function" that infuses syntax with semantics
+@[command_elab colors] def elabColors : CommandElab := λ stx => Lean.logInfo "success!"
+```
+
+4. Mathlib has a `#help option` command that displays all options available in the current environment, and their descriptions. `#help option pp.r` will display all options starting with a "pp.r" substring.
+
+Create a `syntax` rule that would accept the following commands:
+
+- `#better_help option`
+- `#better_help option pp.r`
+- `#better_help option some.other.name`
+
+Use the following template:
+
+```
+syntax (name := help) ...
+-- our "elaboration function" that infuses syntax with semantics
+@[command_elab help] def elabHelp : CommandElab := λ stx => Lean.logInfo "success!"
+```
+
+5. Mathlib has a ∑ operator. Create a `syntax` rule that would accept the following terms:
+
+- `∑ x in { 1, 2, 3 }, x^2`
+- `∑ x in { "apple", "banana", "cherry" }, x.length`
+
+Use the following template:
+
+```
+import Std.Classes.SetNotation
+import Std.Util.ExtendedBinder
+syntax (name := bigsumin) ...
+-- our "elaboration function" that infuses syntax with semantics
+@[term_elab bigsumin] def elabSum : TermElab := λ stx tp => return mkNatLit 666
+```
+
+Hint: use the `Std.ExtendedBinder.extBinder` parser.
+Hint: you need Std4 installed in your Lean project for these imports to work.
diff --git a/md/solutions/elaboration.md b/md/solutions/elaboration.md
new file mode 100644
index 0000000..49c3866
--- /dev/null
+++ b/md/solutions/elaboration.md
@@ -0,0 +1,98 @@
+```lean
+import Lean
+open Lean Elab Command Term Meta
+```
+
+## Elaboration: Solutions
+
+### 1.
+
+```lean
+elab n:term "♥" a:"♥"? b:"♥"? : term => do
+  let nExpr : Expr ← elabTermEnsuringType n (mkConst `Nat)
+  if let some a := a then
+    if let some b := b then
+      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 3)
+    else
+      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 2)
+  else
+    return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 1)
+
+#eval 7 ♥ -- 8
+#eval 7 ♥♥ -- 9
+#eval 7 ♥♥♥ -- 10
+```
+
+### 2.
+
+```lean
+-- a) using `syntax` + `@[command_elab alias] def elabOurAlias : CommandElab`
+syntax (name := aliasA) (docComment)? "aliasA " ident " ← " ident* : command
+
+@[command_elab «aliasA»]
+def elabOurAlias : CommandElab := λ stx =>
+  match stx with
+  | `(aliasA $x:ident ← $ys:ident*) =>
+    for y in ys do
+      Lean.logInfo y
+  | _ =>
+    throwUnsupportedSyntax
+
+aliasA hi.hello ← d.d w.w nnn
+
+-- b) using `syntax` + `elab_rules`.
+syntax (name := aliasB) (docComment)? "aliasB " ident " ← " ident* : command
+
+elab_rules : command
+  | `(command | aliasB $m:ident ← $ys:ident*) =>
+    for y in ys do
+      Lean.logInfo y
+
+aliasB hi.hello ← d.d w.w nnn
+
+-- c) using `elab`
+elab "aliasC " x:ident " ← " ys:ident* : command =>
+  for y in ys do
+    Lean.logInfo y
+
+aliasC hi.hello ← d.d w.w nnn
+```
+
+### 3.
+
+```lean
+open Parser.Tactic
+
+-- a) using `syntax` + `@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic`.
+syntax (name := nthRewriteA) "nth_rewriteA " (config)? num rwRuleSeq (ppSpace location)? : tactic
+
+@[tactic nthRewriteA] def elabNthRewrite : Lean.Elab.Tactic.Tactic := fun stx => do
+  match stx with
+  | `(tactic| nth_rewriteA $[$cfg]? $n $rules $_loc) =>
+    Lean.logInfo "rewrite location!"
+  | `(tactic| nth_rewriteA $[$cfg]? $n $rules) =>
+    Lean.logInfo "rewrite target!"
+  | _ =>
+    throwUnsupportedSyntax
+
+-- b) using `syntax` + `elab_rules`.
+syntax (name := nthRewriteB) "nth_rewriteB " (config)? num rwRuleSeq (ppSpace location)? : tactic
+
+elab_rules (kind := nthRewriteB) : tactic
+  | `(tactic| nth_rewriteB $[$cfg]? $n $rules $_loc) =>
+    Lean.logInfo "rewrite location!"
+  | `(tactic| nth_rewriteB $[$cfg]? $n $rules) =>
+    Lean.logInfo "rewrite target!"
+
+-- c) using `elab`.
+elab "nth_rewriteC " (config)? num rwRuleSeq loc:(ppSpace location)? : tactic =>
+  if let some loc := loc then
+    Lean.logInfo "rewrite location!"
+  else
+    Lean.logInfo "rewrite target!"
+
+example : 2 + 2 = 4 := by
+  nth_rewriteC 2 [← add_zero] at h
+  nth_rewriteC 2 [← add_zero]
+  sorry
+```
diff --git a/md/solutions/expressions.md b/md/solutions/expressions.md
index 9a352c9..e095448 100644
--- a/md/solutions/expressions.md
+++ b/md/solutions/expressions.md
@@ -7,7 +7,7 @@ open Lean Meta
 
 ## Expressions: Solutions
 
-1. Create expression `1 + 2` with `Expr.app`.
+### 1.
 
 ```lean
 def one : Expr :=
@@ -18,7 +18,7 @@ elab "one" : term => return one
 #reduce one -- 3
 ```
 
-2. Create expression `1 + 2` with `Lean.mkAppN`.
+### 2.
 
 ```lean
 def two : Expr :=
@@ -29,7 +29,7 @@ elab "two" : term => return two
 #reduce two -- 3
 ```
 
-3. Create expression `λ x => 1 + x`.
+### 3.
 
 ```lean
 def three : Expr :=
@@ -42,7 +42,7 @@ elab "three" : term => return three
 #reduce three 6 -- 7
 ```
 
-4. [**De Bruijn Indexes**] Create expression `λ a, λ b, λ c, (b * a) + c`.
+### 4.
 
 ```lean
 def four : Expr :=
@@ -70,7 +70,7 @@ elab "four" : term => return four
 #reduce four 666 1 2 -- 668
 ```
 
-5. Create expression `λ x y => x + y`.
+### 5.
 
 ```lean
 def five :=
@@ -87,7 +87,7 @@ elab "five" : term => return five
 #reduce five 4 5 -- 9
 ```
 
-6. Create expression `λ x, String.append "hello, " x`.
+### 6.
 
 ```lean
 def six :=
@@ -100,7 +100,7 @@ elab "six" : term => return six
 #eval six "world" -- "Hello, world"
 ```
 
-7. Create expression `∀ x : Prop, x ∧ x`.
+### 7.
 
 ```lean
 def seven : Expr :=
@@ -113,7 +113,7 @@ elab "seven" : term => return seven
 #reduce seven -- ∀ (x : Prop), x ∧ x
 ```
 
-8. Create expression `Nat → String`.
+### 8.
 
 ```lean
 def eight : Expr :=
@@ -126,7 +126,7 @@ elab "eight" : term => return eight
 #reduce eight -- Nat → String
 ```
 
-9. Create expression `λ (p : Prop) => (λ hP : p => hP)`.
+### 9.
 
 ```lean
 def nine : Expr :=
@@ -143,7 +143,7 @@ elab "nine" : term => return nine
 #reduce nine -- fun p hP => hP
 ```
 
-10. [**Universe levels**] Create expression `Type 6`.
+### 10.
 
 ```lean
 def ten : Expr :=
diff --git a/md/solutions/metam.md b/md/solutions/metam.md
index ab11480..eea169f 100644
--- a/md/solutions/metam.md
+++ b/md/solutions/metam.md
@@ -5,8 +5,7 @@ open Lean Meta
 
 ## `MetaM`: Solutions
 
-1. [**Metavariables**] Create a metavariable with type `Nat`, and assign to it value `3`.
-Notice that changing the type of the metavarible from `Nat` to, for example, `String`, doesn't raise any errors - that's why, as was mentioned, we must make sure *"(a) that `val` must have the target type of `mvarId` and (b) that `val` must only contain `fvars` from the local context of `mvarId`".*
+### 1.
 
 ```lean
 #eval show MetaM Unit from do
@@ -17,7 +16,7 @@ Notice that changing the type of the metavarible from `Nat` to, for example, `St
   IO.println s!"value in hi: {← instantiateMVars hi}" -- Nat.succ Nat.zero
 ```
 
-2. [**Metavariables**] What would `instantiateMVars (Lean.mkAppN (Expr.const 'Nat.add []) #[mkNatLit 1, mkNatLit 2])` output?
+### 2.
 
 ```lean
 -- It would output the same expression we gave it - there were no metavariables to instantiate.
@@ -26,7 +25,7 @@ Notice that changing the type of the metavarible from `Nat` to, for example, `St
   IO.println instantiatedExpr -- fun (x : Nat) => x
 ```
 
-3. [**Metavariables**] Fill in the missing lines in the following code. ...
+### 3.
 
 ```lean
 #eval show MetaM Unit from do
@@ -51,10 +50,7 @@ Notice that changing the type of the metavarible from `Nat` to, for example, `St
   IO.println instantiatedMvar1 -- Nat.add (Nat.add 2 ?_uniq.2) 1
 ```
 
-4. [**Metavariables**] Consider the theorem `red`, and tactic `explore` below.  
-a) What would be the `type` and `userName` of metavariable `mvarId`?  
-b) What would be the `type`s and `userName`s of all local declarations in this metavariable's local context?  
-Print them all out. ...
+### 4.
 
 ```lean
 elab "explore" : tactic => do
@@ -81,7 +77,7 @@ theorem red (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by
   sorry
 ```
 
-5. [**Metavariables**] Write a tactic `solve` that proves the theorem `red`.
+### 5.
 
 ```lean
 -- The type of our metavariable `2 + 2`. We want to find a `localDecl` that has the same type, and `assign` our metavariable to that `localDecl`.
@@ -98,17 +94,14 @@ theorem redSolved (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by
   solve
 ```
 
-6. [**Computation**] What is the normal form of the following expressions:  
-a) `λ x => x` of type `Bool → Bool`  
-b) `(λ x => x) ((true && false) || true)` of type `Bool`  
-c) `800 + 2` of type `Nat`
+### 6.
 
 ```lean
-def sixA : Bool → Bool := λ x => x
+def sixA : Bool → Bool := fun x => x
 -- .lam `x (.const `Bool []) (.bvar 0) (Lean.BinderInfo.default)
 #eval Lean.Meta.reduce (Expr.const `sixA [])
 
-def sixB : Bool := (λ x => x) ((true && false) || true)
+def sixB : Bool := (fun x => x) ((true && false) || true)
 -- .const `Bool.true []
 #eval Lean.Meta.reduce (Expr.const `sixB [])
 
@@ -117,7 +110,7 @@ def sixC : Nat := 800 + 2
 #eval Lean.Meta.reduce (Expr.const `sixC [])
 ```
 
-7. [**Computation**] Show that `1` created with `Expr.lit (Lean.Literal.natVal 1)` is definitionally equal to an expression created with `Expr.app (Expr.const ``Nat.succ []) (Expr.const ``Nat.zero [])`.
+### 7.
 
 ```lean
 #eval show MetaM Unit from do
@@ -128,18 +121,12 @@ def sixC : Nat := 800 + 2
   IO.println isEqual -- true
 ```
 
-8. [**Computation**] Determine whether the following expressions are definitionally equal. If `Lean.Meta.isDefEq` succeeds, and it leads to metavariable assignment, write down the assignments.  
-a) `5 =?= (λ x => 5) ((λ y : Nat → Nat => y) (λ z : Nat => z))`  
-b) `2 + 1 =?= 1 + 2`  
-c) `?a =?= 2`, where `?a` has a type `String`  
-d) `?a + Int =?= "hi" + ?b`, where `?a` and `?b` don't have a type  
-e) `2 + ?a =?= 3`  
-f) `2 + ?a =?= 2 + 1`
+### 8.
 
 ```lean
--- a) `5 =?= (λ x => 5) ((λ y : Nat → Nat => y) (λ z : Nat => z))`
+-- a) `5 =?= (fun x => 5) ((fun y : Nat → Nat => y) (fun z : Nat => z))`
 -- Definitionally equal.
-def expr2 := (λ x => 5) ((λ y : Nat → Nat => y) (λ z : Nat => z))
+def expr2 := (fun x => 5) ((fun y : Nat → Nat => y) (fun z : Nat => z))
 #eval show MetaM Unit from do
   let expr1 := Lean.mkNatLit 5
   let expr2 := Expr.const `expr2 []
@@ -198,7 +185,7 @@ def expr2 := (λ x => 5) ((λ y : Nat → Nat => y) (λ z : Nat => z))
   IO.println s!"a: {← instantiateMVars a}"
 ```
 
-9. [**Computation**] Write down what you expect the following code to output. ...
+### 9.
 
 ```lean
 @[reducible] def reducibleDef     : Nat := 1 -- same as `abbrev`
@@ -232,10 +219,7 @@ def defaultDef                    : Nat := 3
   dbg_trace (← ppExpr reducedExpr) -- [1, 2, 3, irreducibleDef]
 ```
 
-10. [**Constructing Expressions**] Create expression `λ x, 1 + x` in two ways:  
-a) not idiomatically, with loose bound variables  
-b) idiomatically.  
-In what version can you use `Lean.mkAppN`? In what version can you use `Lean.Meta.mkAppM`?
+### 10.
 
 ```lean
 -- Non-idiomatic: we can only use `Lean.mkAppN`.
@@ -245,7 +229,7 @@ def tenA : MetaM Expr := do
 
 -- Idiomatic: we can use both `Lean.mkAppN` and `Lean.Meta.mkAppM`.
 def tenB : MetaM Expr := do
-  Lean.Meta.withLocalDecl `x .default (Expr.const `Nat []) (λ x => do
+  Lean.Meta.withLocalDecl `x .default (Expr.const `Nat []) (fun x => do
     -- let body := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkNatLit 1, x]
     let body ← Lean.Meta.mkAppM `Nat.add #[Lean.mkNatLit 1, x]
     Lean.Meta.mkLambdaFVars #[x] body
@@ -257,7 +241,7 @@ def tenB : MetaM Expr := do
   ppExpr (← tenB) -- fun x => Nat.add 1 x
 ```
 
-11. [**Constructing Expressions**] Create expression `∀ (yellow: Nat), yellow`.
+### 11.
 
 ```lean
 def eleven : MetaM Expr :=
@@ -267,10 +251,7 @@ def eleven : MetaM Expr :=
   dbg_trace (← eleven) -- forall (yellow : Nat), yellow
 ```
 
-12. [**Constructing Expressions**] Create expression `∀ (n : Nat), n = n + 1` in two ways:  
-a) not idiomatically, with loose bound variables  
-b) idiomatically.  
-In what version can you use `Lean.mkApp3`? In what version can you use `Lean.Meta.mkEq`?
+### 12.
 
 ```lean
 -- Non-idiomatic: we can only use `Lean.mkApp3`.
@@ -282,7 +263,7 @@ def twelveA : MetaM Expr := do
 
 -- Idiomatic: we can use both `Lean.mkApp3` and `Lean.Meta.mkEq`.
 def twelveB : MetaM Expr := do
-  withLocalDecl `n BinderInfo.default (Expr.const `Nat []) (λ x => do
+  withLocalDecl `n BinderInfo.default (Expr.const `Nat []) (fun x => do
     let nPlusOne := Expr.app (Expr.app (Expr.const `Nat.add []) x) (Lean.mkNatLit 1)
     -- let forAllBody := Lean.mkApp3 (Expr.const ``Eq []) (Expr.const `Nat []) x nPlusOne
     let forAllBody ← Lean.Meta.mkEq x nPlusOne
@@ -297,12 +278,12 @@ def twelveB : MetaM Expr := do
   ppExpr (← twelveB) -- ∀ (n : Nat), n = Nat.add n 1
 ```
 
-13. [**Constructing Expressions**] Create expression `λ (f : Nat → Nat), ∀ (n : Nat), f n = f (n + 1)` idiomatically.
+### 13.
 
 ```lean
 def thirteen : MetaM Expr := do
-  withLocalDecl `f BinderInfo.default (Expr.forallE `a (Expr.const `Nat []) (Expr.const `Nat []) .default) (λ y => do
-    let lamBody ← withLocalDecl `n BinderInfo.default (Expr.const `Nat []) (λ x => do
+  withLocalDecl `f BinderInfo.default (Expr.forallE `a (Expr.const `Nat []) (Expr.const `Nat []) .default) (fun y => do
+    let lamBody ← withLocalDecl `n BinderInfo.default (Expr.const `Nat []) (fun x => do
       let fn := Expr.app y x
       let fnPlusOne := Expr.app y (Expr.app (Expr.app (Expr.const `Nat.add []) (x)) (Lean.mkNatLit 1))
       let forAllBody := mkApp3 (mkConst ``Eq []) (Expr.const `Nat []) fn fnPlusOne
@@ -317,7 +298,7 @@ def thirteen : MetaM Expr := do
   ppExpr (← thirteen) -- fun f => (n : Nat) → Eq Nat (f n) (f (Nat.add n 1))
 ```
 
-14. [**Constructing Expressions**] What would you expect the output of the following code to be?...
+### 14.
 
 ```lean
 #eval show Lean.Elab.Term.TermElabM _ from do
@@ -334,8 +315,7 @@ def thirteen : MetaM Expr := do
   dbg_trace conclusion -- forall (a.1 : Prop) (b.1 : Prop), (Or a.1 b.1) -> b.1 -> (And a.1 a.1)
 ```
 
-15. [**Backtracking**] Check that the expressions `?a + Int` and `"hi" + ?b` are definitionally equal with `isDefEq` (make sure to use the proper types or `Option.none` for the types of your metavariables!).
-Use `saveState` and `restoreState` to revert metavariable assignments.
+### 15.
 
 ```lean
 #eval show MetaM Unit from do
diff --git a/md/solutions/syntax.md b/md/solutions/syntax.md
new file mode 100644
index 0000000..323da1f
--- /dev/null
+++ b/md/solutions/syntax.md
@@ -0,0 +1,92 @@
+```lean
+import Lean
+import Lean.Parser.Syntax
+
+open Lean Elab Command Term
+```
+
+## `Syntax`: Solutions
+
+### 1.
+
+```lean
+namespace a
+  scoped notation:71 lhs:50 " 💀 " rhs:72 => lhs - rhs
+end a
+
+namespace b
+  set_option quotPrecheck false
+  scoped infixl:71 " 💀 " => fun lhs rhs => lhs - rhs
+end b
+
+namespace c
+  scoped syntax:71 term:50 " 💀 " term:72 : term
+  scoped macro_rules | `($l:term 💀 $r:term) => `($l - $r)
+end c
+
+open a
+#eval 5 * 8 💀 4 -- 20
+#eval 8 💀 6 💀 1 -- 1
+```
+
+### 2.
+
+```lean
+syntax "good morning" : term
+syntax "hello" : command
+syntax "yellow" : tactic
+
+-- Note: the following are highlighted in red, however that's just because we haven't implemented the semantics ("elaboration function") yet - the syntax parsing stage works.
+
+#eval good morning -- works
+-- good morning -- error: `expected command`
+
+hello -- works
+-- #eval hello -- error: `expected term`
+
+example : 2 + 2 = 4 := by
+  yellow -- works
+-- yellow -- error: `expected command`
+-- #eval yellow -- error: `unknown identifier 'yellow'`
+```
+
+### 3.
+
+```lean
+syntax (name := colors) (("blue"+) <|> ("red"+)) num : command
+
+@[command_elab colors]
+def elabColors : CommandElab := fun stx => Lean.logInfo "success!"
+
+blue blue 443
+red red red 4
+```
+
+### 4.
+
+```lean
+syntax (name := help) "#better_help" "option" (ident)? : command
+
+@[command_elab help]
+def elabHelp : CommandElab := fun stx => Lean.logInfo "success!"
+
+#better_help option
+#better_help option pp.r
+#better_help option some.other.name
+```
+
+### 5.
+
+```lean
+-- Note: std4 has to be in dependencies of your project for this to work.
+syntax (name := bigsumin) "∑ " Std.ExtendedBinder.extBinder "in " term "," term : term
+
+@[term_elab bigsumin]
+def elabSum : TermElab := fun stx tp =>
+  return mkNatLit 666
+
+#eval ∑ x in { 1, 2, 3 }, x^2
+
+def hi := (∑ x in { "apple", "banana", "cherry" }, x.length) + 1
+#eval hi
+```