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

fix mixup regarding former/later and description of import

Browse source
This commit is contained in:
Jeremy Siek 2020-05-03 15:16:41 -04:00
parent 6a3fec78b6
commit 3d614523dc
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/Inference.lagda.md
View file

@ -260,7 +260,7 @@ open import Relation.Nullary using (¬_; Dec; yes; no)
Once we have a type derivation, it will be easy to construct Once we have a type derivation, it will be easy to construct
from it the intrinsically-typed representation. In order that we from it the intrinsically-typed representation. In order that we
can compare with our previous development, we import can compare with our previous development, we import
module `plfa.part2.DeBruijn`: module `plfa.part2.More`:
``` ```
import plfa.part2.More as DB import plfa.part2.More as DB
@ -462,7 +462,7 @@ corresponding type rule.
The rules are similar to those in The rules are similar to those in
Chapter [Lambda]({{ site.baseurl }}/Lambda/), Chapter [Lambda]({{ site.baseurl }}/Lambda/),
modified to support synthesised and inherited types. modified to support synthesised and inherited types.
The two new rules are those for `⊢↑` and `⊢↓`. The two new rules are those for `⊢↓` and `⊢↑`.
The former both passes the type decoration as the inherited type and returns The former both passes the type decoration as the inherited type and returns
it as the synthesised type. The latter takes the synthesised type and the it as the synthesised type. The latter takes the synthesised type and the
inherited type and confirms they are identical --- it should remind you of inherited type and confirms they are identical --- it should remind you of