From 7c69576733de18357bb0ea804b8c54587c559710 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Thu, 5 Nov 2020 06:09:44 +0100 Subject: [PATCH] Bisimulation: fixes a verb form --- src/plfa/part2/Bisimulation.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part2/Bisimulation.lagda.md b/src/plfa/part2/Bisimulation.lagda.md index b6643798..b9ab227f 100644 --- a/src/plfa/part2/Bisimulation.lagda.md +++ b/src/plfa/part2/Bisimulation.lagda.md @@ -165,7 +165,7 @@ data _~_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where → `let M N ~ (ƛ N†) · M† ``` The language in Chapter [More](/More/) has more constructs, which we could easily add. -However, leaving the simulation small let's us focus on the essence. +However, leaving the simulation small lets us focus on the essence. It's a handy technical trick that we can have a large source language, but only bother to include in the simulation the terms of interest.