I am pleased to announce the source release of Agda 2.3.2! http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Download If you have a recent Haskell Platform installed, you can get it with cabal update cabal install Agda agda-mode setup agda-mode compile (The last step is optional.) Highlights from the release-notes: http://wiki.portal.chalmers.se/agda/uploads/Main.Download/release-notes-2-3-... * A new backend that produces highlighted LaTeX from a literate agda file. * Improved Emacs interaction mode: - No longer depends on GHCi. - Syntax highlighting is updated while buffer is type-checked. - You can case split on several variables simultaneously. * Syntax extensions: - Pattern synonyms. - Qualified mixfix operators. - Sections and instantiated module imports. * Enhancements of the type checker: - Improved coverage checking. - Improved constraint solving and instance search. Enjoy, Andreas (for the Agda team) -- Andreas Abel <>< Du bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.abel@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/