From eaa05fb1dbd9cd4ec91b9565fec2b50feb21d118 Mon Sep 17 00:00:00 2001 From: Mo Mirza Date: Sun, 29 Sep 2019 02:01:42 +0100 Subject: [PATCH] Remove redundant word --- 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 66329705..2d6b7591 100644 --- a/src/plfa/part1/Relations.lagda.md +++ b/src/plfa/part1/Relations.lagda.md @@ -178,7 +178,7 @@ inv-s≤s (s≤s m≤n) = m≤n Here `m≤n` (with no spaces) is a variable name while `m ≤ n` (with spaces) is a type, and the latter is the type of the former. It is a common convention -in Agda to choose derive a variable name by removing +in Agda to derive a variable name by removing spaces from its type. Not every rule is invertible; indeed, the rule for `z≤n` has