From 467f0d11811a4eded261726a7553f175c56a1ca4 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Tue, 29 Sep 2020 12:39:09 +0200 Subject: [PATCH] Revert "Close quotation mark (#521)" (#522) This reverts commit 846a92c14f318f97346b7c41472d1d022fd18319. --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 602dac46..1e92642c 100644 --- a/README.md +++ b/README.md @@ -66,7 +66,7 @@ agda-mode setup To load and type-check the file, use [`C-c C-l`][agda-docs-emacs-notation]. -Agda is edited “interactively”, which means that one can type check code which is not yet complete: if a question mark (?) is used as a placeholder for an expression, and the buffer is then checked, Agda will replace the question mark with a “hole” which can be filled in later. One can also do various other things in the context of a hole: listing the context, inferring the type of an expression, and even evaluating an open term which mentions variables bound in the surrounding context.” +Agda is edited “interactively, which means that one can type check code which is not yet complete: if a question mark (?) is used as a placeholder for an expression, and the buffer is then checked, Agda will replace the question mark with a “hole” which can be filled in later. One can also do various other things in the context of a hole: listing the context, inferring the type of an expression, and even evaluating an open term which mentions variables bound in the surrounding context.” Agda is edited interactively, using “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: