I was mostly thinking of Agda[1] and, to a lesser extent, similar languages like Coq[2] with Proof General[3]. You could write Common Lisp in Notepad if you re

I was mostly thinking of Agda[1] and, to a lesser extent, similar languages like Coq[2] with Proof General[3]. You could write Common Lisp in Notepad if you really wanted to. I do not think using Agda would be at all practical without Emacs. [1]: http://wiki.portal.chalmers.se/agda/pmwiki.php http://wiki.portal.chalmers.se/agda/pmwiki.php [2]: http://coq.inria.fr/ http://coq.inria.fr/ [3]: http://proofgeneral.inf.ed.ac.uk/ http://proofgeneral.inf.ed.ac.uk/