[Agda] Agda 2.3.0 released

[Dominique Devriese]

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?

Thanks
Dominique