From eb3a7276062a5983719e8d073d56aea15bbe0f7b Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Mon, 28 Oct 2019 17:20:44 +0000
Subject: [PATCH 1/3] Consistent import of DB
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

  * Re-export test examples from Chapter DeBruijn in Chapter More.

  * In Chapter Inference, as well as Assignment 4, import the
    instrinsically-typed λ-calculus as follows:
      `import plfa.part2.More as DB`
---
 src/plfa/part2/DeBruijn.lagda.md  |  2 +-
 src/plfa/part2/Inference.lagda.md |  2 +-
 src/plfa/part2/More.lagda.md      | 29 +++++++++++++++++++++++++++++
 3 files changed, 31 insertions(+), 2 deletions(-)

diff --git a/src/plfa/part2/DeBruijn.lagda.md b/src/plfa/part2/DeBruijn.lagda.md
index 82d4a042..29b75d44 100644
--- a/src/plfa/part2/DeBruijn.lagda.md
+++ b/src/plfa/part2/DeBruijn.lagda.md
@@ -449,7 +449,7 @@ _ = ƛ ƛ (# 1 · (# 1 · # 0))
 ```
 
 
-### Test examples
+### Test examples {#examples}
 
 We repeat the test examples from
 Chapter [Lambda]({{ site.baseurl }}/Lambda/).
diff --git a/src/plfa/part2/Inference.lagda.md b/src/plfa/part2/Inference.lagda.md
index cd89e5c4..e70962dd 100644
--- a/src/plfa/part2/Inference.lagda.md
+++ b/src/plfa/part2/Inference.lagda.md
@@ -263,7 +263,7 @@ can compare with our previous development, we import
 module `plfa.part2.DeBruijn`:
 
 ```
-import plfa.part2.DeBruijn as DB
+import plfa.part2.More as DB
 ```
 
 The phrase `as DB` allows us to refer to definitions
diff --git a/src/plfa/part2/More.lagda.md b/src/plfa/part2/More.lagda.md
index 6f7ffc8b..b1137fee 100644
--- a/src/plfa/part2/More.lagda.md
+++ b/src/plfa/part2/More.lagda.md
@@ -1232,6 +1232,35 @@ Note the arguments need to be swapped and `W` needs to have
 its context adjusted via renaming in order for the right-hand
 side to be well typed.
 
+## Test examples
+
+We repeat the [test examples]({{ site.baseurl }}/DeBruijn/#examples) from Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn),
+in order to make sure we have not broken anything in the process of extending our base calculus.
+```
+two : ∀ {Γ} → Γ ⊢ `ℕ
+two = `suc `suc `zero
+
+plus : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
+plus = μ ƛ ƛ (case (# 1) (# 0) (`suc (# 3 · # 0 · # 1)))
+
+2+2 : ∀ {Γ} → Γ ⊢ `ℕ
+2+2 = plus · two · two
+
+Ch : Type → Type
+Ch A  =  (A ⇒ A) ⇒ A ⇒ A
+
+twoᶜ : ∀ {Γ A} → Γ ⊢ Ch A
+twoᶜ = ƛ ƛ (# 1 · (# 1 · # 0))
+
+plusᶜ : ∀ {Γ A} → Γ ⊢ Ch A ⇒ Ch A ⇒ Ch A
+plusᶜ = ƛ ƛ ƛ ƛ (# 3 · # 1 · (# 2 · # 1 · # 0))
+
+sucᶜ : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ
+sucᶜ = ƛ `suc (# 0)
+
+2+2ᶜ : ∀ {Γ} → Γ ⊢ `ℕ
+2+2ᶜ = plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero
+```
 
 ## Unicode
 

From fbd43ff7a7df5780a7191f27794b4f1901828f20 Mon Sep 17 00:00:00 2001
From: Philip Wadler <wadler@inf.ed.ac.uk>
Date: Fri, 1 Nov 2019 12:03:15 +0000
Subject: [PATCH 2/3] updated mock info

---
 courses/tspl/2019/tspl2019.md | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/courses/tspl/2019/tspl2019.md b/courses/tspl/2019/tspl2019.md
index 1292bd74..d46e5b7c 100644
--- a/courses/tspl/2019/tspl2019.md
+++ b/courses/tspl/2019/tspl2019.md
@@ -91,7 +91,7 @@ Lectures take place Monday, Wednesday, and Friday in AT 5.07.
   <td>11</td>
   <td><b>25 Nov</b> Quantitative (Wen) </td>
   <td><b>27 Nov</b> (no class) </td>
-  <td><b>29 Nov</b> (mock exam) </td> 
+  <td><b>29 Nov</b> Mock Exam </td> 
  </tr>
 </table>
 
@@ -144,6 +144,12 @@ but talk to me if you want to formalise something else.
 
 * Optional project cw6 due 4pm Thursday 28 November (Week 11)
 
+## Mock exam
+
+10am-12noon Friday 29 November, AT 5.05 West Lab. An online
+examination with the Agda proof assistant, under DICE to let you
+practice for the exam and familiarise yourself with exam conditions.
+
 ## Midterm course feedback
 
 You may offer feedback on the course at

From 617fe2a0eed2d732339b75b6d80eef46c3bfabba Mon Sep 17 00:00:00 2001
From: Qais Patankar <qaisjp@gmail.com>
Date: Sat, 2 Nov 2019 14:27:58 +0000
Subject: [PATCH 3/3] Fix missing backtick in Lambda

---
 src/plfa/part2/Lambda.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md
index bd190f55..f5c5616e 100644
--- a/src/plfa/part2/Lambda.lagda.md
+++ b/src/plfa/part2/Lambda.lagda.md
@@ -401,7 +401,7 @@ For instance, we have
 
       (ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) · sucᶜ · `zero
     —→
-      (ƛ "z" ⇒ sucᶜ · (sucᶜ · "z")) · `zero
+      (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero
     —→
       sucᶜ · (sucᶜ · `zero)