The Coq mailing list

["N. Raghavendra" <raghu AT hri.res.in>]

For those who use the el-get package installer for Emacs, there's now an
el-get recipe for agda-input, which installs a single file from the
GitHub Agda repo, and makes it available to Emacs.

agda-input is an input method for typing Unicode characters, especially
mathematical symbols, and may be useful while writing Coq code.  To use
it, put

(setq default-input-method 'Agda)

in your init file.  This enables you to use the Agda input method for
Unicode in any buffer.  Type `C-\' (`toggle-input-method') to activate
the input method, and use its key sequences to input various Unicode
characters.  To deactivate the input method, type `C-\' again.  See

http://people.inf.elte.hu/divip/AgdaTutorial/Symbols.html

for a long list of characters that can be input with this method.  The
canonical Web site is

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.UnicodeInput

The recipe file is at

https://raw.github.com/dimitri/el-get/master/recipes/agda-input.rcp

Cheers,
Raghu.

-- 
N. Raghavendra 
<raghu AT hri.res.in>,
 http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/