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

Further edits

Browse source 
I rearranged the material. It is important that control characters for arrows appear next to the description of arrows.
This commit is contained in:
Philip Wadler 2020-01-10 11:38:28 -03:00 committed by GitHub
parent 6b8e61c1e7
commit 896b2b528a
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 19 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

41
src/plfa/part1/Naturals.lagda.md
View file

@ -965,28 +965,7 @@ 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
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.
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.
How you input the above commands varies according to system and configuration.
The most portable way would be to type `ESC`, `x` and then type
`agda-input-show-translations` or `quail-show-key` literally.
It is important to be familiar with moving cursor in `agda-mode`. 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)
@ -996,3 +975,21 @@ 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.
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.