[Agda] Emacs special character input

Nils Anders Danielsson nad at Cs.Nott.AC.UK
Wed Mar 17 10:49:50 CET 2010


On 2010-03-17 03:44, Carl wrote:
> I'm having a hard time getting Emacs special character input for
> things like \_1 and \r- working. Right now, things are highlighted
> correctly, but if I type a special character sequence it wont get
> automatically converted into a subscript for example. Does anyone know
> how to turn this on.

Does the character ∏ show up in your mode line? In that case the Agda
input method is activated. If not, is the Agda input method
(agda-input.el) installed on your load-path? What happens if you try to
activate it using M-x set-input-method RET Agda RET?

--
/NAD



More information about the Agda mailing list