Made README consistent
This commit is contained in:
parent
cc478e2a6e
commit
a8da92ec08
1 changed files with 8 additions and 8 deletions
16
README.md
16
README.md
|
@ -55,7 +55,7 @@ Once you have installed these tools, you can build the book from source:
|
||||||
|
|
||||||
make build
|
make build
|
||||||
|
|
||||||
You can host your copy of the book locally by running
|
You can host your copy of the book locally by running:
|
||||||
|
|
||||||
make serve
|
make serve
|
||||||
|
|
||||||
|
@ -116,18 +116,18 @@ chapter. For a full list of supported characters, see
|
||||||
|
|
||||||
## Using `agda-mode`
|
## Using `agda-mode`
|
||||||
|
|
||||||
? create hole
|
? hole
|
||||||
{!...!} create hole
|
{!...!} hole with contents
|
||||||
C-c C-l load buffer
|
C-c C-l load buffer
|
||||||
|
|
||||||
Command to give when in a hole:
|
Command to give when in a hole:
|
||||||
|
|
||||||
C-c C-c x split on variable x
|
C-c C-c x split on variable x
|
||||||
C-c C-space fill in hole
|
C-c C-space fill in hole
|
||||||
C-c C-r refine with constructor
|
C-c C-r refine with constructor
|
||||||
C-c C-a automatically fill in hole
|
C-c C-a automatically fill in hole
|
||||||
C-c C-, Goal type and context
|
C-c C-, Goal type and context
|
||||||
C-c C-. Goal type, context, and inferred type
|
C-c C-. Goal type, context, and inferred type
|
||||||
|
|
||||||
See
|
See
|
||||||
[the emacs-mode docs](https://agda.readthedocs.io/en/latest/tools/emacs-mode.html)
|
[the emacs-mode docs](https://agda.readthedocs.io/en/latest/tools/emacs-mode.html)
|
||||||
|
@ -149,7 +149,7 @@ squished beneath it.
|
||||||
## Fonts in Emacs
|
## Fonts in Emacs
|
||||||
|
|
||||||
It is recommended that you add the following to the end of your emacs
|
It is recommended that you add the following to the end of your emacs
|
||||||
configuration file at `~/.emacs`, if you have the named fonts available.
|
configuration file at `~/.emacs`, if you have the mentioned fonts available:
|
||||||
|
|
||||||
``` elisp
|
``` elisp
|
||||||
;; Setting up Fonts for use with Agda/PLFA
|
;; Setting up Fonts for use with Agda/PLFA
|
||||||
|
|
Loading…
Reference in a new issue