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

Fixed module naming typos

Browse source
This commit is contained in:
Reza Gharibi 2019-09-02 23:25:33 +04:30
parent 63fcbbe25e
commit 3a98d1dbae
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
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 `pfla.DeBruijn`: module `plfa.part2.DeBruijn`:
``` ```
import plfa.part2.DeBruijn as DB import plfa.part2.DeBruijn as DB

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

@ -1178,7 +1178,7 @@ the empty type `⊥`. If we use C-c C-n to normalise the term
Agda will return an answer warning us that the impossible has occurred: Agda will return an answer warning us that the impossible has occurred:
⊥-elim (.plfa.Lambda.impossible "a" "a" refl) ⊥-elim (plfa.part2.Lambda.impossible "a" "a" refl)
While postulating the impossible is a useful technique, it must be While postulating the impossible is a useful technique, it must be
used with care, since such postulation could allow us to provide used with care, since such postulation could allow us to provide