Show Menu
Cheatography

Agda Emacs Keyboard Shortcuts by [deleted]

Emacs bindings for Agda sourced from http://agda.readthedocs.io/en/v2.5.2/tools/emacs-mode.html

Global Context

C-c C-l
Load file
C-c C-x C-c
Co­mpile file
C-c C-x C-q
Quit, kill the Agda process
C-c C-x C-r
Kill and re­start the Agda process
C-c C-x C-d
Remove goals and highli­ghting (d­eac­tivate)
C-c C-x C-h
Toggle display of hidden arguments
C-c C-=
Show constr­aints
C-c C-s
Solve constr­aints
C-c C-?
Show all goals
C-c C-f
Move to next goal (f­orward)
C-c C-b
Move to previous goal (b­ack­wards)
C-c C-d
Infer (d­educe) type
C-c C-o
Module co­ntents
C-c C-z
Search through defini­tions in scope
C-c C-n
Compute normal form
C-u C-c C-n
Compute normal form, ignoring abstract
C-u C-u C-c C-n
Compute and print normal form of show <ex­pre­ssi­on>
C-c C-x M-;
Commen­t/u­nco­mment rest of buffer
C-c C-x C-s
Switch to a different Agda version

Input

M-x descri­be-­inp­ut-­method Agda
View all characters you can input using the Agda input method
C-x 8 RET
Input unicode by symbol descri­ption
 

Goal Context

C-c C-SPC
Give (fill goal)
C-c C-r
Re­fine. Partial give: makes new holes for missing arguments
C-c C-a
Automatic Proof Search (Auto)
C-c C-c
Case split
C-c C-h
Compute type of helper function and add type signature to kill ring (clipb­oard)
C-c C-t
Goal type
C-c C-e
Context (e­nvi­ron­ment)
C-c C-d
Infer (d­educe) type
C-c C-,
Goal type and context
C-c C-.
Goal type, context and inferred type
C-c C-o
Module co­ntents
C-c C-n
Compute normal form
C-u C-c C-n
Compute normal form, ignoring abstract
C-u C-u C-c C-n
Compute and print normal form of show <ex­pre­ssi­on>

Other Commands

TAB
Indent current line, cycles between points
S-TAB
Indent current line, cycles in opposite direction
M-.
Go to definition of identifier under point
Middle mouse button
Go to definition of identifier clicked on
M-*
Go back (Emacs < 25.1)
M-,
Go back (Emacs >= 25.1)
 

Comments

No comments yet. Add yours below!

Add a Comment

Your Comment

Please enter your name.

    Please enter your email address

      Please enter your Comment.