From 896b2b528a98da51545f3fb267df673718048787 Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Fri, 10 Jan 2020 11:38:28 -0300 Subject: [PATCH] Further edits I rearranged the material. It is important that control characters for arrows appear next to the description of arrows. --- src/plfa/part1/Naturals.lagda.md | 41 +++++++++++++++----------------- 1 file changed, 19 insertions(+), 22 deletions(-) diff --git a/src/plfa/part1/Naturals.lagda.md b/src/plfa/part1/Naturals.lagda.md index 15bf9e9f..1444ecd9 100644 --- a/src/plfa/part1/Naturals.lagda.md +++ b/src/plfa/part1/Naturals.lagda.md @@ -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 where you navigated to the last time, and starts with the same character next time. The command `\l` works similarly for left arrows. - -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 +In place of left, right, up, and down keys, one may also use control characters: 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 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.