[Agda] Simple Agda Libraries

[Nils Anders Danielsson]

On 2009-01-12 10:57, Nils Anders Danielsson wrote:
>
> 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.

I should add that this input method is enabled by default (as indicated
by a ∏ sign in the Emacs mode line). If the input method is not enabled,
then you are either using an old version of the Emacs mode, or you have
manually told Emacs to use a different input method (perhaps by using
set-input-method somewhere in your .emacs).

-- 
/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.