diff --git a/src/plfa/part1/Relations.lagda.md b/src/plfa/part1/Relations.lagda.md index b9e3ab335..35460b45b 100644 --- a/src/plfa/part1/Relations.lagda.md +++ b/src/plfa/part1/Relations.lagda.md @@ -15,7 +15,7 @@ the next step is to define relations, such as _less than or equal_. ```agda import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; cong) -open import Data.Nat using (ℕ; zero; suc; _+_) +open import Data.Nat using (ℕ; zero; suc; _+_; _*_) open import Data.Nat.Properties using (+-comm; +-identityʳ) ```