C-c C-l |
Load file
|
C-c C-x C-c |
Compile file
|
C-c C-x C-q |
Quit, kill the Agda process
|
C-c C-x C-r |
Kill and restart the Agda process
|
C-c C-x C-d |
Remove goals and highlighting (deactivate)
|
C-c C-x C-h |
Toggle display of hidden arguments
|
C-c C-= |
Show constraints
|
C-c C-s |
Solve constraints
|
C-c C-? |
Show all goals
|
C-c C-f |
Move to next goal (forward)
|
C-c C-b |
Move to previous goal (backwards)
|
C-c C-d |
Infer (deduce) type
|
C-c C-o |
Module contents
|
C-c C-z |
Search through definitions 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 <expression> |
C-c C-x M-; |
Comment/uncomment rest of buffer
|
C-c C-x C-s |
Switch to a different Agda version
|
M-x describe-input-method Agda |
View all characters you can input using the Agda input method
|
C-x 8 RET |
Input unicode by symbol description
|
C-c C-SPC |
Give (fill goal)
|
C-c C-r |
Refine. 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 (clipboard)
|
C-c C-t |
Goal type
|
C-c C-e |
Context (environment)
|
C-c C-d |
Infer (deduce) type
|
C-c C-, |
Goal type and context
|
C-c C-. |
Goal type, context and inferred type
|
C-c C-o |
Module contents
|
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 <expression> |
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)
|
No comments yet.
Cheatography n. The art of mapping complex subjects into clear, instantly navigable reference guides.
