[Agda] Agda 2.3.0 released

[Ulf Norell]

On Wed, Nov 23, 2011 at 2:06 PM, Dominique Devriese <
dominique.devriese at cs.kuleuven.be> wrote:

> Ulf, all,
>
> Thanks and congrats everyone for the effort put into this release, the
> amount of new features is impressive. One thing is not clear to me in
> the release notes:
>
> > * New more liberal syntax for mutually recursive definitions.
> > It is no longer necessary to use the 'mutual' keyword to define
> > mutually recursive functions or datatypes. Instead, it is enough to
> > declare things before they are used. Instead of ...
>
> > * Unsolved meta-variables are now frozen after every mutual block.
>
> How do these two interact? When are the meta-vars frozen now? Are
> mutual block boundaries inferred somehow perhaps?
>

Yes, mutual block boundaries are inferred. A mutual block starts with a
type signature and ends when there are no type signatures still waiting for
a definition.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20111123/8c7612d2/attachment.html