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

Merge pull request #395 from h4iku/fix-name-typo

Browse source 
Fixed module naming typos
This commit is contained in:
Philip Wadler 2019-09-04 12:56:00 +01:00 committed by GitHub
commit 68a128e819
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
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
from it the intrinsically-typed representation. In order that we
can compare with our previous development, we import
module `pfla.DeBruijn`:
module `plfa.part2.DeBruijn`:
```
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:
⊥-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
used with care, since such postulation could allow us to provide