Show Menu
Cheatography
  1. Home >
  2. Cheat Sheets >

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
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 highli­ghting (deactivate)
 
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 (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 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
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 (clipb­oard)
 
C-c C-t
Goal type
 
C-c C-e
Context (environ­ment)
 
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 <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)
 

Metadata

  • Languages:
  • Published: 30th July, 2017

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.