Skip to content

Commit

Permalink
Update README.md (#959)
Browse files Browse the repository at this point in the history
Fixed a typo.

Co-authored-by: Wen Kokke <[email protected]>
  • Loading branch information
Ninijura and wenkokke authored Feb 28, 2024
1 parent 4a87c23 commit 9609226
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -164,7 +164,7 @@ Open the first chapter of the book (`plfa/src/plfa/part1/Naturals.lagda.md`) in

To load and type-check the file, use [`C-c C-l`][agda-readthedocs-emacs-notation].

Agda is edited interactively, using [“holes”][agda-readthedocs-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-readthedocs-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 do while the cursor is in a hole:

- `C-c C-c`: **c**ase split (asks for variable name)
- `C-c C-space`: fill in hole
Expand Down

0 comments on commit 9609226

Please sign in to comment.