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

Fix typos (#508)

Browse source
This commit is contained in:
Gagan Devagiri 2020-08-19 22:27:52 +01:00 committed by GitHub
parent 9ec78b534d
commit 018113ee02
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/plfa/part3/Compositional.lagda.md
View file

@ -65,7 +65,7 @@ rules `↦-intro`, `⊥-intro`, and `⊔-intro`.
``` ```
If one squints hard enough, the `ℱ` function starts to look like the If one squints hard enough, the `ℱ` function starts to look like the
`curry` operation familar to functional programmers. It turns a `curry` operation familiar to functional programmers. It turns a
function that expects a tuple of length `n + 1` (the environment `Γ , ★`) function that expects a tuple of length `n + 1` (the environment `Γ , ★`)
into a function that expects a tuple of length `n` and returns a into a function that expects a tuple of length `n` and returns a
function of one parameter. function of one parameter.
@ -423,7 +423,7 @@ mean by "context" and "surround".
A _context_ is a program with one hole in it. The following data A _context_ is a program with one hole in it. The following data
definition `Ctx` makes this idea explicit. We index the `Ctx` data definition `Ctx` makes this idea explicit. We index the `Ctx` data
type with two contexts for variables: one for the the hole and one for type with two contexts for variables: one for the hole and one for
terms that result from filling the hole. terms that result from filling the hole.
``` ```