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)

Help Us Go Positive!

We offset our carbon usage with Ecologi. Click the link below to help us!

We offset our carbon footprint via Ecologi
 

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.