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

Add mnemonics to the list of keybindings

Browse source 
Make the mnemonic a little more obvious by bolding the text. Also explain why _split_ is `C-c C-c` [`c` for **c**case].
This commit is contained in:
Siddharth 2020-10-03 13:06:02 +05:30 committed by GitHub
parent 47d08d71fb
commit f9b5ad3091
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 6 additions and 6 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:
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.