michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fixes to TSPL 2019

Browse source
This commit is contained in:
wadler 2019-09-15 17:15:46 +01:00
parent db46fd1539
commit bf8b03c67f
4 changed files with 21 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
courses/tspl/2018/Assignment3.lagda.md
View file

@ -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"

4
courses/tspl/2018/Assignment4.lagda.md
View file

@ -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 ∥⁺

32
courses/tspl/2019/tspl2019.md
View file

@ -26,9 +26,9 @@ Lectures take place Monday, Wednesday, and Friday in AT 5.07. (Room provisional.
</tr>
<tr>
<td>1</td>
<td><b>16 Sep</b> <a href="{{ site.baseurl }}/part1/Naturals/">Naturals</a></td>
<td><b>18 Sep</b> <a href="{{ site.baseurl }}/part1/Induction/">Induction</a></td>
<td><b>20 Sep</b> <a href="{{ site.baseurl }}/part1/Relations/">Relations</a></td>
<td><b>16 Sep</b> <a href="{{ site.baseurl }}/Naturals/">Naturals</a></td>
<td><b>18 Sep</b> <a href="{{ site.baseurl }}/Induction/">Induction</a></td>
<td><b>20 Sep</b> <a href="{{ site.baseurl }}/Relations/">Relations</a></td>
</tr>
<tr>
<td>2</td>
@ -38,40 +38,40 @@ Lectures take place Monday, Wednesday, and Friday in AT 5.07. (Room provisional.
</tr>
<tr>
<td>3</td>
<td><b>30 Oct</b> <a href="{{ site.baseurl }}/part1/Equality/">Equality</a> &amp;
<td><b>30 Oct</b> <a href="{{ site.baseurl }}/Equality/">Equality</a> &amp;
<a href="{{ site.baseurl }}/Isomorphism/">Isomorphism</a></td>
<td><b>2 Oct</b> <a href="{{ site.baseurl }}/part1/Connectives/">Connectives</a></td>
<td><b>4 Oct</b> <a href="{{ site.baseurl }}/part1/Negation/">Negation</a></td>
<td><b>2 Oct</b> <a href="{{ site.baseurl }}/Connectives/">Connectives</a></td>
<td><b>4 Oct</b> <a href="{{ site.baseurl }}/Negation/">Negation</a></td>
</tr>
<tr>
<td>4</td>
<td><b>7 Oct</b> <a href="{{ site.baseurl }}/part1/Quantifiers/">Quantifiers</a></td>
<td><b>9 Oct</b> <a href="{{ site.baseurl }}/part1/Decidable/">Decidable</a></td>
<td><b>7 Oct</b> <a href="{{ site.baseurl }}/Quantifiers/">Quantifiers</a></td>
<td><b>9 Oct</b> <a href="{{ site.baseurl }}/Decidable/">Decidable</a></td>
<td><b>11 Oct</b> (tutorial only)</td>
</tr>
<tr>
<td>5</td>
<td><b>14 Oct</b> <a href="{{ site.baseurl }}/part1/Lists/">Lists</a></td>
<td><b>14 Oct</b> <a href="{{ site.baseurl }}/Lists/">Lists</a></td>
<td><b>16 Oct</b> <!-- (tutorial only) --></td>
<td><b>18 Oct</b> <!-- <a href="{{ site.baseurl }}/part1/Lists/">Lists</a> --></td>
<td><b>18 Oct</b> <!-- <a href="{{ site.baseurl }}/Lists/">Lists</a> --></td>
</tr>
<tr>
<td>6</td>
<td><b>21 Oct</b> <!-- <a href="{{ site.baseurl }}/part1/Lambda/">Lambda</a> --></td>
<td><b>21 Oct</b> <!-- <a href="{{ site.baseurl }}/Lambda/">Lambda</a> --></td>
<td><b>23 Oct</b> <!-- (no class) --></td>
<td><b>25 Oct</b> <!-- <a href="{{ site.baseurl }}/part1/Properties/">Properties</a> --></td>
<td><b>25 Oct</b> <!-- <a href="{{ site.baseurl }}/Properties/">Properties</a> --></td>
</tr>
<tr>
<td>7</td>
<td><b>28 Oct</b> <!-- <a href="{{ site.baseurl }}/part1/DeBruijn/">DeBruijn</a> --></td>
<td><b>30 Oct</b> <!-- <a href="{{ site.baseurl }}/part1/More/">More</a> --></td>
<td><b>1 Nov</b> <!-- <a href="{{ site.baseurl }}/part1/Inference/">Inference</a> --></td>
<td><b>28 Oct</b> <!-- <a href="{{ site.baseurl }}/DeBruijn/">DeBruijn</a> --></td>
<td><b>30 Oct</b> <!-- <a href="{{ site.baseurl }}/More/">More</a> --></td>
<td><b>1 Nov</b> <!-- <a href="{{ site.baseurl }}/Inference/">Inference</a> --></td>
</tr>
<tr>
<td>8</td>
<td><b>4 Nov</b> <!-- (no class) --></td>
<td><b>6 Nov</b> <!-- (tutorial only) --></td>
<td><b>8 Nov</b> <!-- <a href="{{ site.baseurl }}/part1/Untyped/">Untyped</a> --></td>
<td><b>8 Nov</b> <!-- <a href="{{ site.baseurl }}/Untyped/">Untyped</a> --></td>
</tr>
<tr>
<td>9</td>

3
index.md
View file

@ -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