diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 0000000..e094246
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,31 @@
+name: CI
+
+on:
+  pull_request:
+  push:
+    branches:
+      - master
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - name: checkout
+        uses: actions/checkout@v4
+
+      - name: install elan
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain $(cat lean-toolchain)
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: Cache dependencies
+        uses: actions/cache@v3
+        with:
+          path: .lake
+          key: deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
+          restore-keys: |
+            deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}
+
+      - name: lake build
+        run: lake build --quiet
\ No newline at end of file
diff --git a/lake-manifest.json b/lake-manifest.json
index 4de7f9d..caf5715 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,10 +4,19 @@
  [{"url": "https://github.com/Seasawher/mdgen",
    "type": "git",
    "subDir": null,
-   "rev": "c501f6b8fa2502362bf94678d404857e46e2b65d",
+   "rev": "2c641fe54d48a5d4adff3a78dbc4a50c5f76b0c0",
    "name": "mdgen",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "c501f6b8fa2502362bf94678d404857e46e2b65d",
+   "inputRev": "v1.3.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.7.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "«lean4-metaprogramming-book»",
diff --git a/lakefile.lean b/lakefile.lean
index 4a50e87..c84ca45 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,12 +4,15 @@ open Lake DSL
 package «lean4-metaprogramming-book» where
   srcDir := "lean"
 
+@[default_target]
 lean_lib «lean4-metaprogramming-book» where
   roots := #[`cover, `extra, `main, `solutions]
   globs := #[Glob.one `cover, Glob.submodules `extra, Glob.submodules `main, Glob.submodules `solutions]
 
 require mdgen from git
-  "https://github.com/Seasawher/mdgen" @ "c501f6b8fa2502362bf94678d404857e46e2b65d"
+  "https://github.com/Seasawher/mdgen" @ "v1.3.0"
+
+require std from git "https://github.com/leanprover/std4" @ "v4.7.0"
 
 def runCmd (cmd : String) (args : Array String) : ScriptM Bool := do
   let out ← IO.Process.output {
diff --git a/lean-toolchain b/lean-toolchain
index 26638e0..9ad3040 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.4.0
+leanprover/lean4:v4.7.0
diff --git a/lean/main/01_intro.lean b/lean/main/01_intro.lean
index 7ee2679..3401465 100644
--- a/lean/main/01_intro.lean
+++ b/lean/main/01_intro.lean
@@ -128,8 +128,13 @@ elab "#assertType " termStx:term " : " typeStx:term : command =>
       logInfo "success"
     catch | _ => throwError "failure"
 
-#assertType 5  : Nat -- success
-#assertType [] : Nat -- failure
+/-- info: success -/
+#guard_msgs in --#
+#assertType 5  : Nat
+
+/-- error: failure -/
+#guard_msgs in --#
+#assertType [] : Nat
 
 /-! We started by using `elab` to define a `command` syntax. When parsed
 by the compiler, it will trigger the incoming computation.
diff --git a/lean/main/04_metam.lean b/lean/main/04_metam.lean
index 4ff970d..4265ebb 100644
--- a/lean/main/04_metam.lean
+++ b/lean/main/04_metam.lean
@@ -127,7 +127,7 @@ assigns `?b := f a`. Assigned metavariables are not considered open goals, so
 the only goal that remains is `?m3`.
 
 Now the third `apply` comes in. Since `?b` has been assigned, the target of
-`?m3` is now `f (f a) = a`. Again, the application of `h` succeeds and the
+`?m3` is now `f a = a`. Again, the application of `h` succeeds and the
 tactic assigns `?m3 := h a`.
 
 At this point, all metavariables are assigned as follows:
@@ -1235,9 +1235,9 @@ Notice that changing the type of the metavariable from `Nat` to, for example, `S
       -- 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?  
+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.
 
     ```lean
@@ -1256,17 +1256,17 @@ Notice that changing the type of the metavariable from `Nat` to, for example, `S
       sorry
     ```
 5. [**Metavariables**] Write a tactic `solve` that proves the theorem `red`.
-6. [**Computation**] What is the normal form of the following expressions:  
-  **a)** `fun x => x` of type `Bool → Bool`  
-  **b)** `(fun x => x) ((true && false) || true)` of type `Bool`  
+6. [**Computation**] What is the normal form of the following expressions:
+  **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 =?= (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`  
+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 =?= (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.
 
@@ -1300,14 +1300,14 @@ Notice that changing the type of the metavariable from `Nat` to, for example, `S
       let reducedExpr ← Meta.reduce constantExpr
       dbg_trace (← ppExpr reducedExpr) -- ...
     ```
-10. [**Constructing Expressions**] Create expression `fun 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.  
+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`?
 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/05_syntax.lean b/lean/main/05_syntax.lean
index 0543da0..b091548 100644
--- a/lean/main/05_syntax.lean
+++ b/lean/main/05_syntax.lean
@@ -154,10 +154,12 @@ We can now write `MyTerm` in place of things like `1 + 1` and it will be
 it just means that the Lean parser can understand it:
 -/
 
-def Playground1.test := MyTerm
+#check_failure MyTerm
 -- elaboration function for 'termMyTerm' has not been implemented
 --   MyTerm
 
+/-! Note: `#check_failure` command allows incorrectly typed terms to be indicated without error. -/
+
 /-!
 Implementing this so-called "elaboration function", which will actually
 give meaning to this syntax in terms of Lean's fundamental `Expr` type,
@@ -182,7 +184,7 @@ scoped syntax "⊥" : term -- ⊥ for false
 scoped syntax "⊤" : term -- ⊤ for true
 scoped syntax:40 term " OR " term : term
 scoped syntax:50 term " AND " term : term
-#check ⊥ OR (⊤ AND ⊥) -- elaboration function hasn't been implemented but parsing passes
+#check_failure ⊥ OR (⊤ AND ⊥) -- elaboration function hasn't been implemented but parsing passes
 
 end Playground2
 
@@ -203,9 +205,11 @@ syntax:50 boolean_expr " AND " boolean_expr : boolean_expr
 Now that we are working in our own syntax category, we are completely
 disconnected from the rest of the system. And these cannot be used in place of
 terms anymore:
--/
 
+```lean
 #check ⊥ AND ⊤ -- expected term
+```
+-/
 
 /-!
 In order to integrate our syntax category into the rest of the system we will
@@ -214,7 +218,7 @@ will re-embed it into the `term` category:
 -/
 
 syntax "[Bool|" boolean_expr "]" : term
-#check [Bool| ⊥ AND ⊤] -- elaboration function hasn't been implemented but parsing passes
+#check_failure [Bool| ⊥ AND ⊤] -- elaboration function hasn't been implemented but parsing passes
 
 /-!
 ### Syntax combinators
@@ -272,15 +276,17 @@ syntax binNumber := binDigit,+
 /-!
 Since we can just use named parsers in place of syntax categories, we can now easily
 add this to the `term` category:
--/
 
+```lean
 syntax "bin(" binNumber ")" : term
 #check bin(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
 #check bin() -- fails to parse because `binNumber` is "one or many": expected 'O' or 'Z'
+```
+-/
 
 syntax binNumber' := binDigit,* -- note the *
 syntax "emptyBin(" binNumber' ")" : term
-#check emptyBin() -- elaboration function hasn't been implemented but parsing passes
+#check_failure emptyBin() -- elaboration function hasn't been implemented but parsing passes
 
 /-!
 Note that nothing is limiting us to only using one syntax combinator per parser,
@@ -288,7 +294,7 @@ we could also have written all of this inline:
 -/
 
 syntax "binCompact(" ("Z" <|> "O"),+ ")" : term
-#check binCompact(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
+#check_failure binCompact(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
 
 /-!
 As a final feature, let's add an optional string comment that explains the binary
@@ -297,8 +303,8 @@ literal being declared:
 
 -- The (...)? syntax means that the part in parentheses is optional
 syntax "binDoc(" (str ";")? binNumber ")" : term
-#check binDoc(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
-#check binDoc("mycomment"; Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
+#check_failure binDoc(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
+#check_failure binDoc("mycomment"; Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
 
 /-!
 ## Operating on Syntax
@@ -559,15 +565,15 @@ the bound variables, we refer the reader to the macro chapter.
 
 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.  
+    **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.
 
-    ```
+    ```lean
       syntax "good morning" : term
       syntax "hello" : command
       syntax "yellow" : tactic
diff --git a/lean/main/06_macros.lean b/lean/main/06_macros.lean
index 4af95e8..d00d69f 100644
--- a/lean/main/06_macros.lean
+++ b/lean/main/06_macros.lean
@@ -35,7 +35,7 @@ to indicate that "it doesn't feel responsible for this syntax". In this case
 it's merely used to fill a wildcard pattern that should never be reached anyways.
 
 However we can in fact register multiple macros for the same syntax this way
-if we desire, they will be tried one after another (the later registered ones have 
+if we desire, they will be tried one after another (the later registered ones have
 higher priority)  -- is "higher" correct?
 until one throws either a real error using `Macro.throwError` or succeeds, that
 is it does not `Macro.throwUnsupported`. Let's see this in action:
@@ -169,7 +169,7 @@ for example macro creating macros, we can escape the anti quotation using: `` `(
 If we want to specify the syntax kind we wish `x` to be interpreted as
 we can make this explicit using: `` `($x:term) `` where `term` can be
 replaced with any other valid syntax category (e.g. `command`) or parser
-(e.g. `ident`). 
+(e.g. `ident`).
 
 So far this is only a more formal explanation of the intuitive things
 we've already seen in the syntax chapter and up to now in this chapter,
@@ -198,11 +198,11 @@ For example:
 -/
 
 -- syntactically cut away the first element of a tuple if possible
-syntax "cut_tuple " "(" term ", " term,+ ")" : term 
+syntax "cut_tuple " "(" term ", " term,+ ")" : term
 
 macro_rules
   -- cutting away one element of a pair isn't possible, it would not result in a tuple
-  | `(cut_tuple ($x, $y)) => `(($x, $y)) 
+  | `(cut_tuple ($x, $y)) => `(($x, $y))
   | `(cut_tuple ($x, $y, $xs,*)) => `(($y, $xs,*))
 
 #check cut_tuple (1, 2) -- (1, 2) : Nat × Nat
@@ -225,7 +225,7 @@ we know so far we'd have to write two `macro_rules` now, one for the case
 with, one for the case without the optional argument. However the rest
 of the syntactic translation works exactly the same with and without
 the optional argument so what we can do using a splice here is to essentially
-define both cases at once: 
+define both cases at once:
 -/
 
 macro_rules
@@ -410,8 +410,8 @@ macro_rules
   -- in this case `error_position`, giving it the name `tk`
   | `(error_position%$tk first) => withRef tk (Macro.throwError "Ahhh")
 
-#eval error_position all -- the error is indicated at `error_position all`
-#eval error_position first -- the error is only indicated at `error_position`
+#check_failure error_position all -- the error is indicated at `error_position all`
+#check_failure error_position first -- the error is only indicated at `error_position`
 
 /-
 Obviously controlling the positions of errors in this way is quite important
diff --git a/lean/main/07_elaboration.lean b/lean/main/07_elaboration.lean
index c8d8328..ac904c9 100644
--- a/lean/main/07_elaboration.lean
+++ b/lean/main/07_elaboration.lean
@@ -173,7 +173,7 @@ elab "#findCElab " c:command : command => do
 /-!
 TODO: Maybe we should also add a mini project that demonstrates a
 non # style command aka a declaration, although nothing comes to mind right now.
-TODO:  Define a `conjecture` declaration, similar to `lemma/theorem`, except that 
+TODO:  Define a `conjecture` declaration, similar to `lemma/theorem`, except that
 it is automatically sorried.  The `sorry` could be a custom one, to reflect that
 the "conjecture" might be expected to be true.
 -/
@@ -260,7 +260,7 @@ this information to complete elaboration.
 We can also easily provoke cases where this does not work out. For example:
 -/
 
-#check set_option trace.Elab.postpone true in List.foldr .add
+#check_failure set_option trace.Elab.postpone true in List.foldr .add
 -- [Elab.postpone] .add : ?m.5808 → ?m.5809 → ?m.5809
 -- invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant
   -- ?m.5808 → ?m.5809 → ?m.5809
@@ -316,7 +316,7 @@ def myanonImpl : TermElab := fun stx typ? => do
   -- Term elaborators can only postpone execution once, so the elaborator
   -- doesn't end up in an infinite loop. Hence, we only try to postpone it,
   -- otherwise we may cause an error.
-  tryPostponeIfNoneOrMVar typ? 
+  tryPostponeIfNoneOrMVar typ?
   -- If we haven't found the type after postponing just error
   let some typ := typ? | throwError "expected type must be known"
   if typ.isMVar then
@@ -328,9 +328,9 @@ def myanonImpl : TermElab := fun stx typ? => do
   elabTerm stx typ -- call term elaboration recursively
 
 #check (⟨⟨1, sorry⟩⟩ : Fin 12) -- { val := 1, isLt := (_ : 1 < 12) } : Fin 12
-#check ⟨⟨1, sorry⟩⟩ -- expected type must be known
-#check (⟨⟨0⟩⟩ : Nat) -- type doesn't have exactly one constructor
-#check (⟨⟨⟩⟩ : Nat → Nat) -- type is not of the expected form: Nat -> Nat
+#check_failure ⟨⟨1, sorry⟩⟩ -- expected type must be known
+#check_failure (⟨⟨0⟩⟩ : Nat) -- type doesn't have exactly one constructor
+#check_failure (⟨⟨⟩⟩ : Nat → Nat) -- type is not of the expected form: Nat -> Nat
 
 /-!
 As a final note, we can shorten the postponing act by using an additional
@@ -338,7 +338,7 @@ 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 
+elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do
   sorry
 
 
@@ -377,8 +377,8 @@ elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do
 
     Please add these semantics:
 
-    **a)** using `syntax` + `@[command_elab alias] def elabOurAlias : CommandElab`.  
-    **b)** using `syntax` + `elab_rules`.  
+    **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`.
@@ -392,8 +392,8 @@ elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do
 
     Please add these semantics:
 
-    **a)** using `syntax` + `@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic`.  
-    **b)** using `syntax` + `elab_rules`.  
+    **a)** using `syntax` + `@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic`.
+    **b)** using `syntax` + `elab_rules`.
     **c)** using `elab`.
 
 -/
diff --git a/lean/main/09_tactics.lean b/lean/main/09_tactics.lean
index 208c009..2a8f990 100644
--- a/lean/main/09_tactics.lean
+++ b/lean/main/09_tactics.lean
@@ -39,9 +39,10 @@ We start by simply declaring the tactic with no implementation:
 
 syntax "custom_tactic" : tactic
 
+/-- error: tactic 'tacticCustom_tactic' has not been implemented -/
+#guard_msgs in --#
 example : 42 = 42 := by
   custom_tactic
--- tactic 'tacticCustom_tactic' has not been implemented
   sorry
 
 /-
@@ -60,11 +61,13 @@ example : 42 = 42 := by
 We can now try a harder problem, that cannot be immediately dispatched by `rfl`:
 -/
 
-example : 43 = 43 ∧ 42 = 42:= by
-  custom_tactic
--- tactic 'rfl' failed, equality expected
---   43 = 43 ∧ 42 = 42
--- ⊢ 43 = 43 ∧ 42 = 42
+#check_failure (by custom_tactic : 42 = 43 ∧ 42 = 42)
+-- type mismatch
+--   Iff.rfl
+-- has type
+--   ?m.1437 ↔ ?m.1437 : Prop
+-- but is expected to have type
+--   42 = 43 ∧ 42 = 42 : Prop
 
 /-
 We extend the `custom_tactic` tactic with a tactic that tries to break `And`
@@ -142,6 +145,7 @@ elab "custom_sorry_0" : tactic => do
 example : 1 = 2 := by
   custom_sorry_0
 -- unsolved goals: ⊢ 1 = 2
+  sorry
 
 /-
 This defines a syntax extension to Lean, where we are naming the piece of syntax
@@ -172,6 +176,7 @@ example : 1 = 2 := by
   custom_sorry_1
 -- goal type: Eq.{1} Nat (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))
 -- unsolved goals: ⊢ 1 = 2
+  sorry
 
 /-
 To `sorry` the goal, we can use the helper `Lean.Elab.admitGoal`:
@@ -242,6 +247,7 @@ example (H1 : 1 = 1) (H2 : 2 = 2): 2 = 2 := by
 -- H1 : 1 = 1
 -- H2 : 2 = 2
 -- ⊢ 2 = 2
+  sorry
 
 example (H1 : 1 = 1): 2 = 2 := by
   custom_assump_0
@@ -249,6 +255,7 @@ example (H1 : 1 = 1): 2 = 2 := by
 -- unsolved goals
 -- H1 : 1 = 1
 -- ⊢ 2 = 2
+  sorry
 
 /-
 Next, we access the list of hypotheses, which are stored in a data structure
@@ -387,8 +394,7 @@ elab "custom_assump_2" : tactic =>
 example (H1 : 1 = 1) (H2 : 2 = 2) : 2 = 2 := by
   custom_assump_2
 
-example (H1 : 1 = 1): 2 = 2 := by
-  custom_assump_2
+#check_failure (by custom_assump_2 : (H1 : 1 = 1) → 2 = 2)
 -- tactic 'custom_assump_2' failed, unable to find matching hypothesis of type (2 = 2)
 -- H1 : 1 = 1
 -- ⊢ 2 = 2
@@ -466,6 +472,7 @@ theorem test_reverse_goals : (1 = 2 ∧ 3 = 4) ∧ 5 = 6 := by
 -- ⊢ 3 = 4
 -- case left.left
 -- ⊢ 1 = 2
+  all_goals sorry
 
 /-
 ## FAQ
@@ -571,16 +578,11 @@ elab "faq_throw_error" : tactic =>
     let goal ← Lean.Elab.Tactic.getMainGoal
     Lean.Meta.throwTacticEx `faq_throw_error goal "throwing an error at the current goal"
 
-example (b : Bool): b = true := by
-  cases b;
-  faq_throw_error
-  -- case true
-  -- ⊢ true = true
-  -- tactic 'faq_throw_error' failed, throwing an error at the current goal
-  -- case false
-  -- ⊢ false = true
+#check_failure (by faq_throw_error : (b : Bool) → b = true)
+-- tactic 'faq_throw_error' failed, throwing an error at the current goal
+-- ⊢ ∀ (b : Bool), b = true
 
-/-
+/-!
 **Q: What is the difference between `Lean.Elab.Tactic.*` and `Lean.Meta.Tactic.*`?**
 
 A: `Lean.Meta.Tactic.*` contains low level code that uses the `Meta` monad to
@@ -591,9 +593,9 @@ tactic infrastructure and the parsing front-end.
 ## Exercises
 
 1. Consider the theorem `p ∧ q ↔ q ∧ p`. We could either write its proof as a proof term, or construct it using the tactics.
-    When we are writing the proof of this theorem *as a proof term*, we're gradually filling up `_`s with certain expressions, step by step. Each such step corresponds to a tactic.  
+    When we are writing the proof of this theorem *as a proof term*, we're gradually filling up `_`s with certain expressions, step by step. Each such step corresponds to a tactic.
 
-    There are many combinations of steps in which we could write this proof term - but consider the sequence of steps we wrote below. Please write each step as a tactic.  
+    There are many combinations of steps in which we could write this proof term - but consider the sequence of steps we wrote below. Please write each step as a tactic.
     The tactic `step_1` is filled in, please do the same for the remaining tactics (for the sake of the exercise, try to use lower-level apis, such as `mkFreshExprMVar`, `mvarId.assign` and `modify fun _ => { goals := ~)`.
 
     ```lean
@@ -651,7 +653,7 @@ tactic infrastructure and the parsing front-end.
 
       -- 1. Create new `_`s with appropriate types.
       let mvarId1 ← mkFreshExprMVar (Expr.forallE `xxx a b .default) (userName := "red")
-      let mvarId2 ← mkFreshExprMVar (Expr.forallE `yyy b a .default) (userName := "blue") 
+      let mvarId2 ← mkFreshExprMVar (Expr.forallE `yyy b a .default) (userName := "blue")
 
       -- 2. Assign the main goal to the expression `Iff.intro _ _`.
       mvarId.assign (mkAppN (Expr.const `Iff.intro []) #[a, b, mvarId1, mvarId2])
@@ -668,13 +670,13 @@ tactic infrastructure and the parsing front-end.
       step_4
     ```
 
-2. In the first exercise, we used lower-level `modify` api to update our goals.  
-    `liftMetaTactic`, `setGoals`, `appendGoals`, `replaceMainGoal`, `closeMainGoal`, etc. are all syntax sugars on top of `modify fun s : State => { s with goals := myMvarIds }`.  
-    Please rewrite the `forker` tactic with:  
+2. In the first exercise, we used lower-level `modify` api to update our goals.
+    `liftMetaTactic`, `setGoals`, `appendGoals`, `replaceMainGoal`, `closeMainGoal`, etc. are all syntax sugars on top of `modify fun s : State => { s with goals := myMvarIds }`.
+    Please rewrite the `forker` tactic with:
 
-    **a)** `liftMetaTactic`  
-    **b)** `setGoals`  
-    **c)** `replaceMainGoal`  
+    **a)** `liftMetaTactic`
+    **b)** `setGoals`
+    **c)** `replaceMainGoal`
 
     ```lean
     elab "forker" : tactic => do
@@ -707,9 +709,9 @@ tactic infrastructure and the parsing front-end.
 
     For each of the points below, create a tactic `introductor` (one per each point), that turns the goal `(ab: a = b) → (bc: b = c) → (a = c)`:
 
-    **a)** into the goal `(a = c)` with hypotheses `(ab✝: a = b)` and `(bc✝: b = c)`.  
-    **b)** into the goal `(bc: b = c) → (a = c)` with hypothesis `(ab: a = b)`.  
-    **c)** into the goal `(bc: b = c) → (a = c)` with hypothesis `(hello: a = b)`.  
+    **a)** into the goal `(a = c)` with hypotheses `(ab✝: a = b)` and `(bc✝: b = c)`.
+    **b)** into the goal `(bc: b = c) → (a = c)` with hypothesis `(ab: a = b)`.
+    **c)** into the goal `(bc: b = c) → (a = c)` with hypothesis `(hello: a = b)`.
 
     ```lean
     example (a b c : Nat) : (ab: a = b) → (bc: b = c) → (a = c) := by
diff --git a/lean/solutions/05_syntax.lean b/lean/solutions/05_syntax.lean
index 8443ceb..76dea63 100644
--- a/lean/solutions/05_syntax.lean
+++ b/lean/solutions/05_syntax.lean
@@ -1,5 +1,6 @@
 import Lean
 import Lean.Parser.Syntax
+import Std.Util.ExtendedBinder
 
 open Lean Elab Command Term
 
@@ -33,16 +34,18 @@ 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`
+#check_failure good morning -- the syntax parsing stage works
 
-hello -- works
--- #eval hello -- error: `expected term`
+/-- error: elaboration function for 'commandHello' has not been implemented -/
+#guard_msgs in --#
+hello -- the syntax parsing stage works
 
+/-- error: tactic 'tacticYellow' has not been implemented -/
+#guard_msgs in --#
 example : 2 + 2 = 4 := by
-  yellow -- works
--- yellow -- error: `expected command`
--- #eval yellow -- error: `unknown identifier 'yellow'`
+  yellow -- the syntax parsing stage works
+
+#check_failure yellow -- error: `unknown identifier 'yellow'`
 
 /- ### 3. -/