From 849807da580c77f4a5886e65ebe9c15c8a31871b Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Tue, 29 Sep 2020 14:57:07 +0200
Subject: [PATCH] Update README.md
---
README.md | 6 ++----
1 file changed, 2 insertions(+), 4 deletions(-)
diff --git a/README.md b/README.md
index 1e92642c..c10f937a 100644
--- a/README.md
+++ b/README.md
@@ -65,10 +65,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, 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:
+Agda is edited interactively, using [“holes”][agda-docs-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:
C-c C-c x split on variable x
C-c C-space fill in hole
@@ -233,6 +230,7 @@ The EPUB is written to `out/epub/plfa.epub`.
[agda]: https://github.com/agda/agda/releases/tag/v2.6.1
[agda-version]: https://img.shields.io/badge/agda-v2.6.1-blue.svg
+[agda-docs-holes]: https://agda.readthedocs.io/en/v2.5.4/getting-started/quick-guide.html
[agda-docs-emacs-mode]: https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html
[agda-docs-emacs-notation]: https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html#notation-for-key-combinations
[agda-docs-package-system]: https://agda.readthedocs.io/en/v2.6.1/tools/package-system.html#example-using-the-standard-library