Hi all, I gave a demonstration of Agda and its Emacs mode to undergraduates at UIC last week. If anyone's interested in seeing it, it's at: Video: http://www.ethos-os.org/agda.html Code: https://gist.github.com/2004772 Best wishes, Alan.