From 749e6a9e57e1ecfa5ebb0909043d7fc8f6ce98cd Mon Sep 17 00:00:00 2001 From: wadler Date: Mon, 28 Oct 2019 12:00:38 +0000 Subject: [PATCH] renamed exercises --- courses/tspl/2019/tspl2019.md | 1 + src/plfa/part2/Lambda.lagda.md | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/courses/tspl/2019/tspl2019.md b/courses/tspl/2019/tspl2019.md index 911c430b..598bd318 100644 --- a/courses/tspl/2019/tspl2019.md +++ b/courses/tspl/2019/tspl2019.md @@ -148,6 +148,7 @@ but talk to me if you want to formalise something else. You may offer feedback on the course at [https://www.surveymonkey.co.uk/r/YX7ZFYC](https://www.surveymonkey.co.uk/r/YX7ZFYC). + Please do so by 4pm Thursday 31 October. diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md index 95ffff8a..bd190f55 100644 --- a/src/plfa/part2/Lambda.lagda.md +++ b/src/plfa/part2/Lambda.lagda.md @@ -1359,7 +1359,7 @@ or explain why there are no such types. 2. `` ∅ , "x" ⦂ A , "y" ⦂ B ⊢ ƛ "z" ⇒ ` "x" · (` "y" · ` "z") ⦂ C `` -#### Exercise `mul-type` (recommended) +#### Exercise `⊢mul` (recommended) Using the term `mul` you defined earlier, write out the derivation showing that it is well typed. @@ -1369,7 +1369,7 @@ showing that it is well typed. ``` -#### Exercise `mulᶜ-type` (practice) +#### Exercise `⊢mulᶜ` (practice) Using the term `mulᶜ` you defined earlier, write out the derivation showing that it is well typed.