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

Merge pull request #525 from bollu/emacs-keybinds-mnemonics

Browse source 
Add mnemonics when keys are first introduced
This commit is contained in:
Philip Wadler 2020-10-13 12:49:50 +01:00 committed by GitHub
commit 20516d9e8e
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 15 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
README.md
View file

@ -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: 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-c x`: **c**ase split on variable x
C-c C-space fill in hole - `C-c C-space`: fill in hole
C-c C-r refine with constructor - `C-c C-r`: **r**efine with constructor
C-c C-a automatically fill in hole - `C-c C-a`: **a**utomatically fill in hole
C-c C-, goal type and context - `C-c C-,`: goal type and context
C-c C-. goal type, context, and inferred type - `C-c C-.`: goal type, context, and inferred type
See [the emacs-mode docs][agda-docs-emacs-mode] for more details. See [the emacs-mode docs][agda-docs-emacs-mode] for more details.

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

@ -764,8 +764,9 @@ Begin by typing:
The question mark indicates that you would like Agda to help with 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 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 control key while hitting the `c` key followed by the `l` key),
the question mark will be replaced: which stands for **l**oad, the question mark will be
replaced:
_+_ : ℕ → ℕ → ℕ _+_ : ℕ → ℕ → ℕ
m + n = { }0 m + n = { }0
@ -777,11 +778,11 @@ Emacs will also create a window displaying the text
?0 : ℕ ?0 : ℕ
to indicate that hole 0 is to be filled in with a term of type `ℕ`. 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. 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 Move the cursor into the hole and type `C-c C-c` (for **c**ase).
the prompt: You will be given the prompt:
pattern variables to case (empty for split on result): 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 : ℕ n : ℕ
m : ℕ m : ℕ
Going into the hole and type `C-c C-r` will fill it in with a constructor Going into the hole and type `C-c C-r` (for **r**efine) will fill it in
(if there is a unique choice) or tell you what constructors you might use, with a constructor (if there is a unique choice) or tell you what constructors
if there is a choice. In this case, it displays the following: 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 Don't know which constructor to introduce of zero or suc