Emacs and Unicode Commands
emacs but not
so only the
agda shortcuts (below) are relevant.
SPCmeans space bar
Alt-xfor non-Macs and
C-c C-l in Agda files is
Ctrl-c, let go,
For the input of unicode characters go to the end of this page or visit
this site <https://agda.readthedocs.io/en/latest/tools/emacs-mode.html#keybindings>.
General Doom Emacs usage
The ‘ambient mode’ is called evil mode and follows vim-like bindings. The following commands are for evil mode:
SPC h b bto look for bindings (keyboard shortcuts)
SPC f fto find files. can use
TABfor auto-completing paths and
Backspaceto go up a directory
h j k lfor left down up right
SPC b kto kill ‘buffers’ (any little window is a buffer). In general
SPC bgives you many options for buffers.
SPC w kto kill unwanted windows (emacs can get split up into many windows) In general
SPC wgives you many options for windows.
ito go into insert mode (in insert mode you can insert text) and
C-gto go back to evil mode.
C-_to undo (be careful with this, undo can go too far; going into and out of insert mode is considered “one change” in evil mode, so undoing might undo a lot of changes made in insert mode).
rto redo (be careful with this, redo can go too far).
SPC h 'to look up how to write a symbol. (Put your cursor on the symbol first.)
To insert text in the
agda file use
i to enter insert mode.
To escape insert mode do
All the commands below should be done whilst in insert mode.
C-c C-lloads the file
Check the goal :
C-c C-,checks goal of the hole your cursor is in.
Fill the goal :
C-c C-SPCfills hole your cursor is in.
Refine the goal :
C-c C-rrefines the hole your cursor is in.
C-c C-cdoes cases on
xis in the hole your cursor is in.
C-c C-dasks you to give it term / point
x, it deduces the type / space that
C-c C-nasks you to give it term / point
x, it ‘reduces’
xto its ‘simplest (normalised) form’
Looking up definitions : in
agdapad, clicking on something with the wheel of your mouse looks up the definitions of that thing (try clicking on
Typefor example). In
M-SPC c dlooks up the definition of the thing you are hovering over.
You can find more commands for
In general follow the guidance given above to learn unicode commands. However here are some commonly used ones to get you started
\^for superscript, e.g.
You can find more common symbols here.