From aaf5b914b06caa7ada5f4f98e82600f9fd4cdf74 Mon Sep 17 00:00:00 2001 From: Turab Jafri Date: Sun, 25 Aug 2019 22:09:08 -0400 Subject: [PATCH 1/2] part1/Relations: Fix Typo MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit "form `m ≤ n`" -> "from `m ≤ n`" --- src/plfa/part1/Relations.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part1/Relations.lagda.md b/src/plfa/part1/Relations.lagda.md index 1cf5c738b..7e65dc5f0 100644 --- a/src/plfa/part1/Relations.lagda.md +++ b/src/plfa/part1/Relations.lagda.md @@ -161,7 +161,7 @@ Chapter [Decidable]({{ site.baseurl }}/Decidable/). ## Inversion In our defintions, we go from smaller things to larger things. -For instance, form `m ≤ n` we can conclude `suc m ≤ suc n`, +For instance, from `m ≤ n` we can conclude `suc m ≤ suc n`, where `suc m` is bigger than `m` (that is, the former contains the latter), and `suc n` is bigger than `n`. But sometimes we want to go from bigger things to smaller things. From bb5ff4cd6444f8b33ecbaf2a0c942ca0f1008bce Mon Sep 17 00:00:00 2001 From: Turab Jafri Date: Sun, 25 Aug 2019 23:46:15 -0400 Subject: [PATCH 2/2] part1/Relations: Add _*_ import For convenience, readers shouldn't worry about importing functions that are required for exercises --- src/plfa/part1/Relations.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part1/Relations.lagda.md b/src/plfa/part1/Relations.lagda.md index 7e65dc5f0..5dd934165 100644 --- a/src/plfa/part1/Relations.lagda.md +++ b/src/plfa/part1/Relations.lagda.md @@ -18,7 +18,7 @@ the next step is to define relations, such as _less than or equal_. ``` 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) ```