From bf8b03c67f9eb95149f8344c4a0948f9436ce3dc Mon Sep 17 00:00:00 2001 From: wadler Date: Sun, 15 Sep 2019 17:15:46 +0100 Subject: [PATCH] fixes to TSPL 2019 --- courses/tspl/2018/Assignment3.lagda.md | 2 +- courses/tspl/2018/Assignment4.lagda.md | 4 ++-- courses/tspl/2019/tspl2019.md | 32 +++++++++++++------------- index.md | 3 ++- 4 files changed, 21 insertions(+), 20 deletions(-) diff --git a/courses/tspl/2018/Assignment3.lagda.md b/courses/tspl/2018/Assignment3.lagda.md index 3dbcd51c..2cafa1b2 100644 --- a/courses/tspl/2018/Assignment3.lagda.md +++ b/courses/tspl/2018/Assignment3.lagda.md @@ -275,7 +275,7 @@ plus′ : Term plus′ = μ′ + ⇒ ƛ′ m ⇒ ƛ′ n ⇒ case′ m [zero⇒ n - |suc m ⇒ suc (+ · m · n) ] + |suc m ⇒ `suc (+ · m · n) ] where + = ` "+" m = ` "m" diff --git a/courses/tspl/2018/Assignment4.lagda.md b/courses/tspl/2018/Assignment4.lagda.md index 4e4ee525..e28dc4d9 100644 --- a/courses/tspl/2018/Assignment4.lagda.md +++ b/courses/tspl/2018/Assignment4.lagda.md @@ -1077,8 +1077,8 @@ Remember to indent all code by two spaces. ∥ ⊢↓ ⊢M ∥⁺ = ∥ ⊢M ∥⁻ ∥ ⊢ƛ ⊢N ∥⁻ = DB.ƛ ∥ ⊢N ∥⁻ - ∥ ⊢zero ∥⁻ = DB.zero - ∥ ⊢suc ⊢M ∥⁻ = DB.suc ∥ ⊢M ∥⁻ + ∥ ⊢zero ∥⁻ = DB.`zero + ∥ ⊢suc ⊢M ∥⁻ = DB.`suc ∥ ⊢M ∥⁻ ∥ ⊢case ⊢L ⊢M ⊢N ∥⁻ = DB.case ∥ ⊢L ∥⁺ ∥ ⊢M ∥⁻ ∥ ⊢N ∥⁻ ∥ ⊢μ ⊢M ∥⁻ = DB.μ ∥ ⊢M ∥⁻ ∥ ⊢↑ ⊢M refl ∥⁻ = ∥ ⊢M ∥⁺ diff --git a/courses/tspl/2019/tspl2019.md b/courses/tspl/2019/tspl2019.md index e5ceee47..60933813 100644 --- a/courses/tspl/2019/tspl2019.md +++ b/courses/tspl/2019/tspl2019.md @@ -26,9 +26,9 @@ Lectures take place Monday, Wednesday, and Friday in AT 5.07. (Room provisional. 1 - 16 Sep Naturals - 18 Sep Induction - 20 Sep Relations + 16 Sep Naturals + 18 Sep Induction + 20 Sep Relations 2 @@ -38,40 +38,40 @@ Lectures take place Monday, Wednesday, and Friday in AT 5.07. (Room provisional. 3 - 30 Oct Equality & + 30 Oct Equality & Isomorphism - 2 Oct Connectives - 4 Oct Negation + 2 Oct Connectives + 4 Oct Negation 4 - 7 Oct Quantifiers - 9 Oct Decidable + 7 Oct Quantifiers + 9 Oct Decidable 11 Oct (tutorial only) 5 - 14 Oct Lists + 14 Oct Lists 16 Oct - 18 Oct + 18 Oct 6 - 21 Oct + 21 Oct 23 Oct - 25 Oct + 25 Oct 7 - 28 Oct - 30 Oct - 1 Nov + 28 Oct + 30 Oct + 1 Nov 8 4 Nov 6 Nov - 8 Nov + 8 Nov 9 diff --git a/index.md b/index.md index 9f0f35f9..3d16aea2 100644 --- a/index.md +++ b/index.md @@ -49,7 +49,8 @@ Pull requests are encouraged. - Courses taught from the textbook: * Philip Wadler, University of Edinburgh, - [2018]({{ site.baseurl }}/TSPL/2018/) + [2018]({{ site.baseurl }}/TSPL/2018/), + [2019]({{ site.baseurl }}/TSPL/2019/) * David Darais, University of Vermont, [2018](http://david.darais.com/courses/fa2018-cs295A/) * John Leo, Google Seattle, 2018--2019