Bisimulation: fixes a verb form

This commit is contained in:
Marko Dimjašević 2020-11-05 06:09:44 +01:00
parent 9776956c5e
commit 7c69576733
No known key found for this signature in database
GPG key ID: 565EE9641503F0AA

View file

@ -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.