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

Merge pull request #478 from mdimjasevic/lambda-highlighting-1

Browse source 
Lambda: fix highlighting of bindings in the text
This commit is contained in:
Philip Wadler 2020-06-08 08:43:25 +01:00 committed by GitHub
commit 44fb26193f
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/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:
```