michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge pull request #544 from mdimjasevic/bisim-us

Browse source 
Bisimulation: Fixes a Verb Form
This commit is contained in:
Philip Wadler 2020-11-05 10:59:27 +00:00 committed by GitHub
commit a621b7d71e
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/plfa/part2/Bisimulation.lagda.md
View file

@ -165,7 +165,7 @@ data _~_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
→ `let M N ~ (ƛ N†) · M† → `let M N ~ (ƛ N†) · M†
``` ```
The language in Chapter [More](/More/) has more constructs, which we could easily add. 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, 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. but only bother to include in the simulation the terms of interest.