From ebdd29865b815c664e245a3535df8c8650140631 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= <marko@dimjasevic.net>
Date: Thu, 10 Sep 2020 07:39:40 +0200
Subject: [PATCH] Fixes a verb plural error (#512)

---
 src/plfa/part2/DeBruijn.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/plfa/part2/DeBruijn.lagda.md b/src/plfa/part2/DeBruijn.lagda.md
index 309cae55..72bc236a 100644
--- a/src/plfa/part2/DeBruijn.lagda.md
+++ b/src/plfa/part2/DeBruijn.lagda.md
@@ -329,7 +329,7 @@ We write
 
     Γ ⊢ A
 
-for terms which in context `Γ` has type `A`.
+for terms which in context `Γ` have type `A`.
 The judgement is formalised by a datatype indexed
 by a context and a type.
 It looks exactly like the old typing judgment, but