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.