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

Lambda: fix highlighting of bindings in the text

Browse source
This commit is contained in:
Marko Dimjašević 2020-06-07 22:38:34 +02:00
parent 2b0f229c93
commit 3673bc8d26
No known key found for this signature in database
GPG key ID: 565EE9641503F0AA
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/part2/Lambda.lagda.md
View file

@ -1236,8 +1236,8 @@ to use them inside other binding contexts as well as at the top level.
Here the two lookup judgments `∋m` and `∋m′` refer to two different
bindings of variables named `"m"`. In contrast, the two judgments `∋n` and
`∋n′` both refer to the same binding of `"n"` but accessed in different
contexts, the first where "n" is the last binding in the context, and
the second after "m" is bound in the successor branch of the case.
contexts, the first where `"n"` is the last binding in the context, and
the second after `"m"` is bound in the successor branch of the case.
And here are typings for the remainder of the Church example:
```