Skip to content

Commit 9609226

Browse files
Ninijurawenkokke
andauthored
Update README.md (#959)
Fixed a typo. Co-authored-by: Wen Kokke <wenkokke@users.noreply.github.com>
1 parent 4a87c23 commit 9609226

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

README.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -164,7 +164,7 @@ Open the first chapter of the book (`plfa/src/plfa/part1/Naturals.lagda.md`) in
164164

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

167-
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:
167+
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:
168168

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

0 commit comments

Comments
 (0)