From 3d614523dc2f3fcdf3a5e563fce76d6544eaf03f Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Sun, 3 May 2020 15:16:41 -0400 Subject: [PATCH] fix mixup regarding former/later and description of import --- src/plfa/part2/Inference.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/part2/Inference.lagda.md b/src/plfa/part2/Inference.lagda.md index e70962dd..a4ccf4bc 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 `plfa.part2.DeBruijn`: +module `plfa.part2.More`: ``` import plfa.part2.More as DB @@ -462,7 +462,7 @@ corresponding type rule. The rules are similar to those in Chapter [Lambda]({{ site.baseurl }}/Lambda/), 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 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