Emacs interface

Agda comes with an emacs interface written by Dan Synek. To use this interface you have to invoke 'agda-mode', this will be done automatically if the file ends with .agda otherwise write ESC-x agda-mode.

Important Due to a bug in some versions of emacs it is not possible to click into a goal. Try using emacs version 20.3 (emacs-20.3 on our machines) to avoid this problem. If you have problems with this use instead C-c C-f and C-c C-b to move forward respectively backward between the goals.

Last modified: Mon Dec 7 19:13:55 MET 1998