renamed exercises
This commit is contained in:
parent
d2ff9564ce
commit
749e6a9e57
2 changed files with 3 additions and 2 deletions
|
@ -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.
|
||||
|
||||
|
||||
|
|
|
@ -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.
|
||||
|
|
Loading…
Reference in a new issue