[Agda] AIM 9 summary

[Nils Anders Danielsson]

Hi,

Some highlights from AIM 9:

* The wiki is better organised, and some missing pieces have been filled
   in. It is hopefully easier for a newcomer to find relevant
   information now.

* Detailed instructions for how to install Agda on a Mac have been
   written by Shin-Cheng Mu.

* Mutual recursion/corecursion has been implemented by Andreas Abel.

* Ulf has started work on optimising Agda. By using a pointer
   representation of terms we hope to achieve faster equality checks, and
   this representation should also make it easy to switch from
   call-by-name to call-by-need.

* The Emacs mode has been improved: One can compile using C-c C-x C-c.
   More syntax highlighting info is available when there is a type error.
   Left-clicking on an identifier no longer leads to a jump to its
   definition. Restart (C-c C-x C-r) now restarts GHCi. Many commands by
   default normalise (no need for C-u). One can load using C-c C-l.

There were also a number of more applied code sprints. As far as I know
only Conor's ornaments are available to play with so far, but more code
may yet show up.

See the wiki for further details:

 
http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Main.AIM9CodeSprint

-- 
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.