From 3a98d1dbae34019fa15f409f08a1656f15c6edcd Mon Sep 17 00:00:00 2001 From: Reza Gharibi Date: Mon, 2 Sep 2019 23:25:33 +0430 Subject: [PATCH] Fixed module naming typos --- src/plfa/part2/Inference.lagda.md | 2 +- src/plfa/part2/Lambda.lagda.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/part2/Inference.lagda.md b/src/plfa/part2/Inference.lagda.md index bae6e323..654f497b 100644 --- a/src/plfa/part2/Inference.lagda.md +++ b/src/plfa/part2/Inference.lagda.md @@ -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 diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md index a98d3913..cea0bc0f 100644 --- a/src/plfa/part2/Lambda.lagda.md +++ b/src/plfa/part2/Lambda.lagda.md @@ -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