diff --git a/src/plfa/Induction.lagda.md b/src/plfa/Induction.lagda.md
index 953f8d64..6815f776 100644
--- a/src/plfa/Induction.lagda.md
+++ b/src/plfa/Induction.lagda.md
@@ -321,7 +321,7 @@ As a concrete example of how induction corresponds to recursion, here
 is the computation that occurs when instantiating `m` to `2` in the
 proof of associativity.
 
-\begin{code}
+```
 +-assoc-2 : ∀ (n p : ℕ) → (2 + n) + p ≡ 2 + (n + p)
 +-assoc-2 n p =
   begin
@@ -359,7 +359,7 @@ proof of associativity.
       ≡⟨⟩
         0 + (n + p)
       ∎
-\end{code}
+```
 
 
 ## Terminology and notation
diff --git a/src/plfa/Inference.lagda.md b/src/plfa/Inference.lagda.md
index 0d1723fc..a9036d90 100644
--- a/src/plfa/Inference.lagda.md
+++ b/src/plfa/Inference.lagda.md
@@ -250,7 +250,7 @@ We are now ready to begin the formal development.
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
 open import Data.Empty using (⊥; ⊥-elim)
-open import Data.Nat using (ℕ; zero; suc; _+_)
+open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
 open import Data.String using (String; _≟_)
 open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
 open import Relation.Nullary using (¬_; Dec; yes; no)
@@ -1118,9 +1118,9 @@ by inheritance, which is why Agda requires a type declaration for
 those definitions.  A definition with a right-hand side that is a term
 typed by synthesis, such as an application, does not require a type
 declaration.
-\begin{code}
+```
 answer = 6 * 7
-\end{code}
+```
 
 
 ## Unicode