Emacs Mode Key Combinations

This page lists the key bindings of commands specific to (or modified by) the Agda Emacs mode. Standard Emacs commands are not listed.

Note that many commands are modified by prefixing their key combinations with C-u. These commands are listed separately below.

Global commands

    C-c     C-lLoad a file
    C-c C-x C-cCompile a file
    C-c C-x C-qQuit
    C-c C-x C-rKill and restart Agda
    C-c C-x C-dRemove goals and highlighting (deactivate)
    C-c C-x C-hToggle display of hidden arguments
    C-c     C-=Show constraints
    C-c     C-sSolve constraints
    C-c     C-?Show goals
    C-c     C-fNext goal (forward)
    C-c     C-bPrevious goal (back)
    C-c     C-dInfer (deduce) type
C-u C-c     C-dInfer type (normalised)
    C-c     C-oModule contents
    C-c     C-nCompute normal form
C-u C-c     C-nCompute normal form (ignoring abstract)
    C-c C-x M-;Comment/uncomment the rest of the buffer

Commands working in the context of a specific goal

    C-c C-SPCGive
    C-c C-rRefine
    C-c C-aAuto (proof search)
    C-c C-cCase
    C-c C-tGoal type
C-u C-c C-tGoal type (without normalising)
    C-c C-eContext (environment)
C-u C-c C-eContext (without normalising)
    C-c C-dInfer (deduce) type
C-u C-c C-dInfer type (normalised)
    C-c C-,Goal type and context
C-u C-c C-,Goal type and context (without normalising)
    C-c C-.Goal type and inferred type
C-u C-c C-.Goal type and inferred type (without normalising)
    C-c C-oModule contents
    C-c C-nCompute normal form
C-u C-c C-nCompute normal form (ignoring abstract)

Other commands

TABIndent the current line (cycles between positions)
S-TABIndent the current line (cycles in the other direction)
M-.Go to the definition of the identifier under point
Middle mouse buttonGo to the definition of the identifier clicked on
M-*Go back

Howto