Using Abbreviation Mode in Agda

The abbreviation mode makes adding special symbols to Agda very easy, including introducing handcrafted abbreviations for complex symbols used frequently. Some users have increased their usage of special symbols because of the abbreviation mode. (The implementors told us that they discourage the use of the abbreviation mode, and follow the customisation features in How to write Unicode characters. The reason for this is that you cannot use abbreviations in the mini-buffer, which prevents you from searching for these symbols. However, when using query-replace, one can easily work around it by using cut and paste.)

The abbreviation mode is using the Emacs-package "mule", which is activated when following the installation instructions for the emacs mode for Agda.

• To activate the abbreviation mode in Emacs, use the command M-x abbrev-mode. In this mode, an arbitrary sequence of characters (surrounded by blanks and some punctuations) is automatically replaced by other characters. For instance if we want andd to expand to ∧ we do the following:

1. We type in andd.
2. We use the emacs command C-x ail
3. We type in the mini buffer our intended expansion, namely ∧ (typed in using mule as \wedge).

Now whenever we type in a space-like character (blanks and some punctuations) followed by andd followed by a space-like character, then andd is replaced by ∧.

• You can edit the abbreviations you have defined by using M-x edit-abbrevs (when finished use C-c C-c in order to activate your definitions).
• You can prevent the expansion of an abbreviation by using C-q before adding any space-like character after andd.

Put the following in your .emacs file after the lines which load Agda:

   (read-abbrev-file "~/.abbrev_defs")
   (add-hook 'agda2-mode-hook 'abbrev-mode)

These commands load previous abbreviations and save them when exiting Agda. They also activate the abbreviation mode, whenever one enters an Agda file. However, for this to work you need first to create a file ~/.abbrev_defs, which is done by using the following steps:

1. Define at least one abbreviation as above (you can change this abbreviation later by using M-x edit-abbrevs). For instance you can just type in fooo, type in C-x ail, and then type in the Mini-buffer foo, so that fooo is expanded to foo.
2. Then execute M-x write-abbrev-file, and when asked for a file name, enter in the mini-buffer ~/.abbrev_defs
3. Now execute M-x read-abbrev-file, and when asked for a file name, enter in the mini-buffer ~/.abbrev_defs
4. If you now create a new abbreviation, and run C-x s which is the command for saving all buffers, it will ask as well whether you want to save the abbreviation file.

Automatical addition of abbreviations by Agda. Note that Agda automatically adds certain abbreviations. In order to switch them off, execute M-x customize-group and then agda2 and then change the option Agda2 Mode Abbrevs Use Defaults: to No.

General documentation of the Abbreviation mode. More details can be found in the documentation of Emacs under Abbreviation mode in Emacs, also available by C-h i and then switching to the documentation of Emacs, and locating there Abbrevs. (You need to have installed the documentation of Emacs - under Linux install using your distribution the emacs-documentation package).