Merge branch 'dev' of github.com:plfa/plfa.github.io into dev

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>
 
@@ -146,6 +146,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

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/).

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

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)
 

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