The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

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-2.txt

* 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 AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/