From af9b369ea349ed8ced5708bb3bfd685d5ad28d21 Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Sat, 25 May 2019 11:16:08 -0300
Subject: [PATCH] updates to PUC and Assignments

---
 src/plfa/DeBruijn.lagda | 11 ++++++++---
 tspl/PUC.lagda          |  2 +-
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/plfa/DeBruijn.lagda b/src/plfa/DeBruijn.lagda
index d6374ba3..27f4cae7 100644
--- a/src/plfa/DeBruijn.lagda
+++ b/src/plfa/DeBruijn.lagda
@@ -450,10 +450,12 @@ two = `suc `suc `zero
 
 plus : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
 plus = μ ƛ ƛ (case (# 1) (# 0) (`suc (# 3 · # 0 · # 1)))
+
+2+2 : ∀ {Γ} → Γ ⊢ `ℕ
+2+2 = plus · two · two
 \end{code}
-We specify that `two` and `plus` can be typed in an arbitrary environment,
-rather than just the empty environment, because later we will give examples
-where they appear nested inside binders.
+We generalise to arbitrary contexts because later we will give examples
+where `two` appears nested inside binders.
 
 Next, computing two plus two on Church numerals:
 \begin{code}
@@ -468,6 +470,9 @@ plusᶜ = ƛ ƛ ƛ ƛ (# 3 · # 1 · (# 2 · # 1 · # 0))
 
 sucᶜ : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ
 sucᶜ = ƛ `suc (# 0)
+
+2+2ᶜ : ∀ {Γ} → Γ ⊢ `ℕ
+2+2ᶜ = plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero
 \end{code}
 As before we generalise everything to arbitrary
 contexts.  While we are at it, we also generalise `twoᶜ` and
diff --git a/tspl/PUC.lagda b/tspl/PUC.lagda
index 78779c2e..632ece58 100644
--- a/tspl/PUC.lagda
+++ b/tspl/PUC.lagda
@@ -100,6 +100,6 @@ For instructions on how to set up Agda for PLFA see [Getting Started](/GettingSt
   Use file [Exam][Exam]. Despite the rubric, do **all three questions**.
 
 Submit assignments by email to [wadler@inf.ed.ac.uk](mailto:wadler@inf.ed.ac.uk).
-Attach a single file named Assignment1.lagda or the like.  Include
+Attach a single file named `PUC-Assignment1.lagda` or the like.  Include
 your name and email in the submitted file.