The Coq mailing list

[Jelle Herold <jelle AT defekt.nl>]

On Mon, May 09, 2011 at 01:17:48PM +0200, Thomas Strathmann wrote:
> >I still need to find a nice way to do unicode input, my colleagues
> >use ibus or m17n in linux; Do you know of any comparable input
> >methods for the mac?
>
> I've struggled with this problem, too. My solution so far is to use
> the built-in input methods of Emacs in conjunction with some custom
> abbrevs for Unicode symbols I actually use. If someone knows a more
> general way that actually works well I'd be interested.

I've always been quite fond of the Agda input mode for emacs. I did a
quick write-up on how to use it with Proof General.

http://agda.posterous.com/use-agda-input-mode-in-code

FWIW,
Jelle.