The Coq mailing list

[Nils Anders Danielsson <nad AT Cs.Nott.AC.UK>]

On 2010-02-17 13:05, Pierre Courtieu wrote:
> The method of agda is implemented via emacs input methods, it is also
> possible to use this method in proofgeneral and any other emacs mode:
>
> simply type:
> M-x set-input-method <return> TeX <return>

If you replace TeX with Agda you get the actual Agda input method,
assuming that it is installed.

--
/NAD