From 071489c5377927d69636bf67b584764f703376d7 Mon Sep 17 00:00:00 2001 From: Ninijura <31007300+Ninijura@users.noreply.github.com> Date: Tue, 6 Feb 2024 12:47:49 +0100 Subject: [PATCH] Update README.md Fixed a typo. --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 6ca91cbe0..1d3cb0aba 100644 --- a/README.md +++ b/README.md @@ -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