From f9b5ad3091a1a1e381eaf89411ff24c3e3a23971 Mon Sep 17 00:00:00 2001 From: Siddharth Date: Sat, 3 Oct 2020 13:06:02 +0530 Subject: [PATCH 1/2] Add mnemonics to the list of keybindings Make the mnemonic a little more obvious by bolding the text. Also explain why _split_ is `C-c C-c` [`c` for **c**case]. --- README.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index c10f937a..607e53cc 100644 --- a/README.md +++ b/README.md @@ -67,12 +67,12 @@ To load and type-check the file, use [`C-c C-l`][agda-docs-emacs-notation]. Agda is edited interactively, using [“holes”][agda-docs-holes], which are bits of the program that are not yet filled in. If you use a question mark as an expression, and load the buffer using `C-c C-l`, Agda replaces the question mark with a hole. There are several things you can to while the cursor is in a hole: - C-c C-c x split on variable x - C-c C-space fill in hole - C-c C-r refine with constructor - C-c C-a automatically fill in hole - C-c C-, goal type and context - C-c C-. goal type, context, and inferred type +- `C-c C-c x`: **c**ase split on variable x +- `C-c C-space`: fill in hole +- `C-c C-r`: **r**efine with constructor +- `C-c C-a`: **a**utomatically fill in hole +- `C-c C-,`: goal type and context +- `C-c C-.`: goal type, context, and inferred type See [the emacs-mode docs][agda-docs-emacs-mode] for more details. From 242666d380ac5a37181c2573e9d6a639b82c61a9 Mon Sep 17 00:00:00 2001 From: Siddharth Date: Sat, 3 Oct 2020 13:11:18 +0530 Subject: [PATCH 2/2] Mnemonics the first time keys are introduced Add mnemonics for each of the key bindings which have a mnemonic. This makes it easier to learn the bindings. --- src/plfa/part1/Naturals.lagda.md | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/src/plfa/part1/Naturals.lagda.md b/src/plfa/part1/Naturals.lagda.md index 6a4c52a5..27558235 100644 --- a/src/plfa/part1/Naturals.lagda.md +++ b/src/plfa/part1/Naturals.lagda.md @@ -764,8 +764,9 @@ Begin by typing: The question mark indicates that you would like Agda to help with filling in that part of the code. If you type `C-c C-l` (pressing -the control key while hitting the `c` key followed by the `l` key) -the question mark will be replaced: +the control key while hitting the `c` key followed by the `l` key), +which stands for **l**oad, the question mark will be +replaced: _+_ : ℕ → ℕ → ℕ m + n = { }0 @@ -777,11 +778,11 @@ Emacs will also create a window displaying the text ?0 : ℕ to indicate that hole 0 is to be filled in with a term of type `ℕ`. -Typing `C-c C-f` will move you into the next hole. +Typing `C-c C-f` (for **f**orward) will move you into the next hole. We wish to define addition by recursion on the first argument. -Move the cursor into the hole and type `C-c C-c`. You will be given -the prompt: +Move the cursor into the hole and type `C-c C-c` (for **c**ase). +You will be given the prompt: pattern variables to case (empty for split on result): @@ -820,9 +821,9 @@ required type of the hole, and what free variables are available: n : ℕ m : ℕ -Going into the hole and type `C-c C-r` will fill it in with a constructor -(if there is a unique choice) or tell you what constructors you might use, -if there is a choice. In this case, it displays the following: +Going into the hole and type `C-c C-r` (for **r**efine) will fill it in +with a constructor (if there is a unique choice) or tell you what constructors +you might use, if there is a choice. In this case, it displays the following: Don't know which constructor to introduce of zero or suc