From 96092268ca6958cd9b118c7877720209efef24cd Mon Sep 17 00:00:00 2001 From: Kira Kutscher <31007300+Ninijura@users.noreply.github.com> Date: Thu, 29 Feb 2024 00:30:45 +0100 Subject: [PATCH] Update README.md (#959) Fixed a typo. Co-authored-by: Wen Kokke --- 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