[Agda] Simple Agda Libraries

[Nils Anders Danielsson]

On 2009-01-12 10:11, Marcin Benke wrote:
> 
> While I can understand your attitude to the "Unicode madness", let me
> remind you (and other readers of the Agda list) of the TeX input
> method. Enable it and you can type in Unicode whatever (well, most of)
> what you can type in TeX.

Maybe this has not been publicised widely enough, but since July last
year the Emacs mode for Agda comes with a dedicated input method, based
on the TeX input method, which can handle all characters in the standard
libraries and many more.

Furthermore, if you want to find out how to type a given character
(which is present in some Agda file), just put the cursor on it and type
C-u C-x =.

There is more information about this on the wiki (which will hopefully
reappear soon).

-- 
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.