diff --git a/doc/examples/deBruijn.lean b/doc/examples/deBruijn.lean
index a1e6518230..fa83799db2 100644
--- a/doc/examples/deBruijn.lean
+++ b/doc/examples/deBruijn.lean
@@ -153,7 +153,7 @@ use hypotheses such as `a = b` as rewriting/simplications rules.
 We use the `split` to break the nested `match` expression in the `plus` case into two cases.
 The local variables `iha` and `ihb` are the induction hypotheses for `a` and `b`.
 The modifier `←` in a term simplifier argument instructs the term simplier to use the equation as a rewriting rule in
-the "reverse direction. That is, given `h : a = b`, `← h` instructs the term simplifier to rewrite `b` subterms to `a`.
+the "reverse direction". That is, given `h : a = b`, `← h` instructs the term simplifier to rewrite `b` subterms to `a`.
 -/
 theorem Term.constFold_sound (e : Term ctx ty) : e.constFold.denote env = e.denote env := by
   induction e with simp [*]
diff --git a/doc/examples/phoas.lean b/doc/examples/phoas.lean
index 74bc23d674..b599fb7268 100644
--- a/doc/examples/phoas.lean
+++ b/doc/examples/phoas.lean
@@ -23,7 +23,7 @@ We can write a function to translate `Ty` values to a Lean type
 — remember that types are first class, so can be calculated just like any other value.
 We mark `Ty.denote` as `[reducible]` to make sure the typeclass resolution procedure can
 unfold/reduce it. For example, suppose Lean is trying to synthesize a value for the instance
-`Add (Ty.denote Ty.nat)`. Since `Ty.denote` is marked as `[reducible],
+`Add (Ty.denote Ty.nat)`. Since `Ty.denote` is marked as `[reducible]`,
 the typeclass resolution procedure can reduce `Ty.denote Ty.nat` to `Nat`, and use
 the builtin instance for `Add Nat` as the solution.