[Agda] [ANNOUNCE] Agda 2.6.0

[Andres Sicard Ramirez]

Dear all,

The Agda Team is very pleased to announce the release of Agda 2.6.0.

* GHC supported versions

Agda 2.6.0 has been tested with GHC 8.6.4, 8.4.4, 8.2.2, 8.0.2 and
7.10.3 on Linux, macOS and Windows.

Note that this RC cannot be installed on Windows using GHC 8.6.3 due
to a GHC bug.

* Installation

    cabal update && cabal install Agda

* Standard library

A new version of the standard library will be announced soon. For the
time being, you can use the upstream version of the library available
at

    https://github.com/agda/agda-stlib/

* Highlights

** Added support for Cubical Agda
(https://agda.readthedocs.io/en/v2.6.0/language/cubical.html) which
adds new features such as univalence and higher inductive types to
Agda.

** Added support for ML-style automatic generalization of variables
(https://agda.readthedocs.io/en/v2.6.0/language/generalization-of-declared-variables.html).

** Added a new sort `Prop` of definitionally proof-irrelevant
propositions (https://agda.readthedocs.io/en/v2.6.0/language/prop.html).

** The implementation of instance search
(https://agda.readthedocs.io/en/v2.6.0/language/instance-arguments.html)
got a major overhaul and no longer supports overlapping instances
(unless enabled by a flag).

* Complete list of language changes, incompatibilities and closed issues

    http://hackage.haskell.org/package/Agda-2.6.0/changelog

Enjoy Agda 2.6.0.

-- 
Andrés on behalf of the Agda Team