Emacs is the only officially supported interactive Agda environment, as other people have noted. However, I have written a lot of Agda code in other editors (a

Emacs is the only officially supported interactive Agda environment, as other people have noted. However, I have written a lot of Agda code in other editors (acme and vim). It is certainly feasable to do! In fact I find that it improves my code quality not to use the interactive features. When in interactive mode, I blindly chase the goal trying to get the correct type, and often end up going long detours. When I am on my own I get a better overview of the situation, and can often see the shortest path. That said, I wish they would continue to support agda interactive mode on the command line, as it is nice to be able to evaluate expressions in context of a hole. Writing unicode is a breeze with XCompose, in any UTF8-enabled editor. I found a nice XCompose file based on the Plan 9 keyboard file, by Pmarin. It can be downloaded from «Greg 'Groggy' Lehey»'s site: http://www.lemis.com/grog/programs/XCompose http://www.lemis.com/grog/programs/XCompose