merge
This commit is contained in:
commit
435bf28a9e
9 changed files with 60 additions and 20 deletions
|
@ -36,7 +36,7 @@ before_install:
|
||||||
- make travis-setup
|
- make travis-setup
|
||||||
|
|
||||||
script:
|
script:
|
||||||
- curl -L https://raw.githubusercontent.com/MestreLion/git-tools/master/git-restore-mtime | python
|
- travis_retry curl -L https://raw.githubusercontent.com/plfa/git-tools/master/git-restore-mtime | python
|
||||||
- agda --version
|
- agda --version
|
||||||
- acknowledgements --version
|
- acknowledgements --version
|
||||||
- make test-offline # disable to only build cache
|
- make test-offline # disable to only build cache
|
||||||
|
|
19
README.md
19
README.md
|
@ -58,8 +58,23 @@ but Aquamacs users might need to move their startup settings to the Preferences.
|
||||||
|
|
||||||
If you're having trouble typing the Unicode characters into Emacs, the end of
|
If you're having trouble typing the Unicode characters into Emacs, the end of
|
||||||
each chapter should provide a list of the unicode characters introduced in that
|
each chapter should provide a list of the unicode characters introduced in that
|
||||||
chapter. For a full list of supported characters, see
|
chapter.
|
||||||
[agda-input.el](https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el#L194).
|
|
||||||
|
`agda-mode` and emacs have a number of useful commands.
|
||||||
|
Two of them are especially useful when you solve exercises.
|
||||||
|
|
||||||
|
For a full list of supported characters, use `agda-input-show-translations` with:
|
||||||
|
|
||||||
|
M-x agda-input-show-translations
|
||||||
|
|
||||||
|
All the supported characters in `agda-mode` are shown.
|
||||||
|
|
||||||
|
If you want to know how you input a specific Unicode character in agda file,
|
||||||
|
move the cursor onto the character and type the following command:
|
||||||
|
|
||||||
|
M-x quail-show-key
|
||||||
|
|
||||||
|
You'll see the key sequence of the character in mini buffer.
|
||||||
|
|
||||||
|
|
||||||
## Using `agda-mode`
|
## Using `agda-mode`
|
||||||
|
|
5
beta.md
5
beta.md
|
@ -64,7 +64,8 @@ Pull requests are encouraged.
|
||||||
|
|
||||||
- Courses taught from the textbook:
|
- Courses taught from the textbook:
|
||||||
* Philip Wadler, University of Edinburgh,
|
* 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,
|
* David Darais, University of Vermont,
|
||||||
[2018](http://david.darais.com/courses/fa2018-cs295A/)
|
[2018](http://david.darais.com/courses/fa2018-cs295A/)
|
||||||
* John Leo, Google Seattle, 2018--2019
|
* John Leo, Google Seattle, 2018--2019
|
||||||
|
@ -72,6 +73,8 @@ Pull requests are encouraged.
|
||||||
[2019]({{ site.baseurl }}/PUC/2019/)
|
[2019]({{ site.baseurl }}/PUC/2019/)
|
||||||
* Prabhakar Ragde, University of Waterloo,
|
* Prabhakar Ragde, University of Waterloo,
|
||||||
[2019](https://cs.uwaterloo.ca/~plragde/842/)
|
[2019](https://cs.uwaterloo.ca/~plragde/842/)
|
||||||
|
* Jeremy Siek, Indiana University,
|
||||||
|
[2020](https://jsiek.github.io/B522-PL-Foundations/)
|
||||||
- A paper describing the book appeared in [SBMF][sbmf].
|
- A paper describing the book appeared in [SBMF][sbmf].
|
||||||
|
|
||||||
[wen]: https://wenkokke.github.io
|
[wen]: https://wenkokke.github.io
|
||||||
|
|
|
@ -6,7 +6,7 @@
|
||||||
#
|
#
|
||||||
# This script assumes the following folder structure:
|
# This script assumes the following folder structure:
|
||||||
#
|
#
|
||||||
# $DIR/sXXXXXXX/cw$CW/$FILE
|
# $DIR/sXXXXXXX/$CW/$FILE
|
||||||
#
|
#
|
||||||
# The variable DIR refers to the directory passed in as an argument to the
|
# The variable DIR refers to the directory passed in as an argument to the
|
||||||
# script. The variable XXXXXXX refers to the student ID, and it is assumed
|
# script. The variable XXXXXXX refers to the student ID, and it is assumed
|
||||||
|
@ -14,9 +14,9 @@
|
||||||
#
|
#
|
||||||
# sXXXXXXX@sms.ed.ac.uk
|
# sXXXXXXX@sms.ed.ac.uk
|
||||||
#
|
#
|
||||||
# is a valid email address. The variable $CW refers to the number for of the
|
# is a valid email address. The variable $CW refers to the coursework
|
||||||
# coursework of which the students are meant to be notified. The directory
|
# of which the students are meant to be notified (e.g., cw1). The directory
|
||||||
# DIR/sXXXXXXX/cwY/ should only contain a single file, which should be
|
# DIR/sXXXXXXX/$CW/ should only contain a single file, which should be
|
||||||
# specified using the FILE parameter.
|
# specified using the FILE parameter.
|
||||||
#
|
#
|
||||||
# Usage:
|
# Usage:
|
||||||
|
@ -32,12 +32,12 @@ shift
|
||||||
FILE="$1"
|
FILE="$1"
|
||||||
shift
|
shift
|
||||||
|
|
||||||
for ATTACHMENT in "${DIR%/}/s"*"/cw$CW/$FILE"; do
|
for ATTACHMENT in "${DIR%/}/s"*"/$CW/$FILE"; do
|
||||||
SUBJ="Mark for coursework $CW"
|
SUBJ="Mark for coursework $CW"
|
||||||
BODY=""
|
BODY=""
|
||||||
SID=$(echo "$ATTACHMENT" | sed 's|.*/\(s[0-9]\{7\}\)/.*|\1|')
|
SID=$(echo "$ATTACHMENT" | sed 's|.*/\(s[0-9]\{7\}\)/.*|\1|')
|
||||||
ADDR="$SID@sms.ed.ac.uk"
|
ADDR="$SID@sms.ed.ac.uk"
|
||||||
CMD="echo \"$BODY\" | mail -s \"$SUBJ\" -a \"$ATTACHMENT\" \"$ADDR\""
|
CMD="echo \"$BODY\" | mail -c wadler@inf.ed.ac.uk -s \"$SUBJ\" -a \"$ATTACHMENT\" \"$ADDR\""
|
||||||
echo "You are about to run the following command:"
|
echo "You are about to run the following command:"
|
||||||
echo -e "\n$CMD\n"
|
echo -e "\n$CMD\n"
|
||||||
read -p "Are you sure? " -n 1 -r
|
read -p "Are you sure? " -n 1 -r
|
||||||
|
|
6
index.md
6
index.md
|
@ -61,9 +61,15 @@ Pull requests are encouraged.
|
||||||
* Adrian King,
|
* Adrian King,
|
||||||
San Francisco Types, Theorems, and Programming Languages Meetup
|
San Francisco Types, Theorems, and Programming Languages Meetup
|
||||||
[2019-20](http://meet.meetup.com/wf/click?upn=ZDzXt-2B-2BZmzYir6Bq5X7vEQ2iNYdgjN9-2FU9nWKp99AU8rZjrncUsSYODqOGn6kV-2BqW71oirCo-2Bk8O1q2FtDFhYZR-2B737CPhNWBjt58LuSRC-2BWTj61VZCHquysW8z7dVtQWxB5Sorl3chjZLDptP70L7aBZL14FTERnKJcRQdrMtc-3D_IqHN4t3hH47BvE1Cz0BakIxV4odHudhr6IVs-2Fzslmv-2FBuORsh-2FwQmOxMBdyMHsSBndQDQmt47hobqsLp-2Bm04Y9LwgV66MGyucsd0I9EgDEUB-2FjzdtSgRv-2Fxng8Pgsa3AZIEYILOhLpQ5ige5VFYTEHVN1pEqnujCHovmTxJkqAK9H-2BIL15-2FPxx97RfHcz7M30YNyqp6TOYfgTxyUHc6lufYKFA75Y7MV6MeDJMxw9-2FYUxR6CEjdoagQBmaGkBVzN)
|
[2019-20](http://meet.meetup.com/wf/click?upn=ZDzXt-2B-2BZmzYir6Bq5X7vEQ2iNYdgjN9-2FU9nWKp99AU8rZjrncUsSYODqOGn6kV-2BqW71oirCo-2Bk8O1q2FtDFhYZR-2B737CPhNWBjt58LuSRC-2BWTj61VZCHquysW8z7dVtQWxB5Sorl3chjZLDptP70L7aBZL14FTERnKJcRQdrMtc-3D_IqHN4t3hH47BvE1Cz0BakIxV4odHudhr6IVs-2Fzslmv-2FBuORsh-2FwQmOxMBdyMHsSBndQDQmt47hobqsLp-2Bm04Y9LwgV66MGyucsd0I9EgDEUB-2FjzdtSgRv-2Fxng8Pgsa3AZIEYILOhLpQ5ige5VFYTEHVN1pEqnujCHovmTxJkqAK9H-2BIL15-2FPxx97RfHcz7M30YNyqp6TOYfgTxyUHc6lufYKFA75Y7MV6MeDJMxw9-2FYUxR6CEjdoagQBmaGkBVzN)
|
||||||
|
* Jeremy Siek, Indiana University,
|
||||||
|
[2020](https://jsiek.github.io/B522-PL-Foundations/)
|
||||||
- A paper describing the book appeared in [SBMF][sbmf].
|
- A paper describing the book appeared in [SBMF][sbmf].
|
||||||
|
- A notebook version of the textbook
|
||||||
|
is available at [NextJournal][nextjournal].
|
||||||
|
It lets you edit and execute the book via a web interface.
|
||||||
|
|
||||||
[wen]: https://github.com/wenkokke
|
[wen]: https://github.com/wenkokke
|
||||||
[phil]: https://homepages.inf.ed.ac.uk/wadler/
|
[phil]: https://homepages.inf.ed.ac.uk/wadler/
|
||||||
[GitHub]: https://github.com/plfa/plfa.github.io/
|
[GitHub]: https://github.com/plfa/plfa.github.io/
|
||||||
[sbmf]: https://homepages.inf.ed.ac.uk/wadler/topics/agda.html#sbmf
|
[sbmf]: https://homepages.inf.ed.ac.uk/wadler/topics/agda.html#sbmf
|
||||||
|
[nextjournal]: https://nextjournal.com/plfa/ToC
|
||||||
|
|
|
@ -353,6 +353,7 @@ reverse of the second appended to the reverse of the first:
|
||||||
|
|
||||||
reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
|
reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
|
||||||
|
|
||||||
|
|
||||||
#### Exercise `reverse-involutive` (recommended)
|
#### Exercise `reverse-involutive` (recommended)
|
||||||
|
|
||||||
A function is an _involution_ if when applied twice it acts
|
A function is an _involution_ if when applied twice it acts
|
||||||
|
|
|
@ -965,8 +965,8 @@ After typing `\r`, one can access the many available arrows by using
|
||||||
the left, right, up, and down keys to navigate. The command remembers
|
the left, right, up, and down keys to navigate. The command remembers
|
||||||
where you navigated to the last time, and starts with the same
|
where you navigated to the last time, and starts with the same
|
||||||
character next time. The command `\l` works similarly for left arrows.
|
character next time. The command `\l` works similarly for left arrows.
|
||||||
|
In place of left, right, up, and down keys, one may also use control
|
||||||
In place of left, right, up, and down keys, one may also use control characters:
|
characters:
|
||||||
|
|
||||||
C-b left (backward one character)
|
C-b left (backward one character)
|
||||||
C-f right (forward one character)
|
C-f right (forward one character)
|
||||||
|
@ -975,3 +975,18 @@ In place of left, right, up, and down keys, one may also use control characters:
|
||||||
|
|
||||||
We write `C-b` to stand for control-b, and similarly. One can also navigate
|
We write `C-b` to stand for control-b, and similarly. One can also navigate
|
||||||
left and right by typing the digits that appear in the displayed list.
|
left and right by typing the digits that appear in the displayed list.
|
||||||
|
|
||||||
|
For a full list of supported characters, use `agda-input-show-translations` with:
|
||||||
|
|
||||||
|
M-x agda-input-show-translations
|
||||||
|
|
||||||
|
All the characters supported by `agda-mode` are shown. We write M-x to stand for
|
||||||
|
typing `ESC` followed by `x`.
|
||||||
|
|
||||||
|
If you want to know how you input a specific Unicode character in an agda file,
|
||||||
|
move the cursor onto the character and use `quail-show-key` with:
|
||||||
|
|
||||||
|
M-x quail-show-key
|
||||||
|
|
||||||
|
You'll see a key sequence of the character in mini buffer.
|
||||||
|
If you run `M-x qualy-show-key` on say `∸`, you will see `\.-` for the character.
|
||||||
|
|
|
@ -72,7 +72,7 @@ Terms have seven constructs. Three are for the core lambda calculus:
|
||||||
Three are for the naturals:
|
Three are for the naturals:
|
||||||
|
|
||||||
* Zero `` `zero ``
|
* Zero `` `zero ``
|
||||||
* Successor `` `suc ``
|
* Successor `` `suc M ``
|
||||||
* Case `` case L [zero⇒ M |suc x ⇒ N ] ``
|
* Case `` case L [zero⇒ M |suc x ⇒ N ] ``
|
||||||
|
|
||||||
And one is for recursion:
|
And one is for recursion:
|
||||||
|
@ -1315,7 +1315,7 @@ there is at most one `A` such that the judgment holds:
|
||||||
```
|
```
|
||||||
|
|
||||||
The typing relation `Γ ⊢ M ⦂ A` is not injective. For example, in any `Γ`
|
The typing relation `Γ ⊢ M ⦂ A` is not injective. For example, in any `Γ`
|
||||||
the term `ƛ "x" ⇒ "x"` has type `A ⇒ A` for any type `A`.
|
the term `` ƛ "x" ⇒ ` "x" `` has type `A ⇒ A` for any type `A`.
|
||||||
|
|
||||||
### Non-examples
|
### Non-examples
|
||||||
|
|
||||||
|
|
|
@ -568,7 +568,7 @@ swap {Γ} {x} {y} {M} {A} {B} {C} x≢y ⊢M = rename ρ ⊢M
|
||||||
--------------------------
|
--------------------------
|
||||||
→ Γ , x ⦂ A , y ⦂ B ∋ z ⦂ C
|
→ Γ , x ⦂ A , y ⦂ B ∋ z ⦂ C
|
||||||
ρ Z = S x≢y Z
|
ρ Z = S x≢y Z
|
||||||
ρ (S y≢x Z) = Z
|
ρ (S z≢x Z) = Z
|
||||||
ρ (S z≢x (S z≢y ∋z)) = S z≢y (S z≢x ∋z)
|
ρ (S z≢x (S z≢y ∋z)) = S z≢y (S z≢x ∋z)
|
||||||
```
|
```
|
||||||
Here the renaming map takes a variable at the end into a variable one
|
Here the renaming map takes a variable at the end into a variable one
|
||||||
|
@ -742,8 +742,8 @@ Now that naming is resolved, let's unpack the first three cases:
|
||||||
|
|
||||||
∅ ⊢ V ⦂ B
|
∅ ⊢ V ⦂ B
|
||||||
Γ , x ⦂ A , y ⦂ B ⊢ N ⦂ C
|
Γ , x ⦂ A , y ⦂ B ⊢ N ⦂ C
|
||||||
------------------------------------
|
----------------------------
|
||||||
Γ , x ⦂ A , y ⦂ B ⊢ N [ y := V ] ⦂ C
|
Γ , x ⦂ A ⊢ N [ y := V ] ⦂ C
|
||||||
|
|
||||||
The typing rule for abstractions then yields the required conclusion.
|
The typing rule for abstractions then yields the required conclusion.
|
||||||
|
|
||||||
|
|
Loading…
Add table
Reference in a new issue