[Agda] [ ANNOUNCE ] Standard library v1.7 - release candidate 1

Matthew Daggitt matthewdaggitt at gmail.com
Thu May 27 08:25:09 CEST 2021


Dear all,

The Agda Team is pleased to announce the first release candidate for
version 1.7 of the standard library. The release candidate has been
tested using the first release candidate of Agda 2.6.2. This release
includes many new features, the highlights of which are:


   - New module for making system calls during type checking,
Reflection.External, which re-exports
Agda.Builtin.Reflection.External.
   - New predicate for lists that are enumerations of their type in
Data.List.Relation.Unary.Enumerates.
   - New weak induction schemes in Data.Fin.Induction that allows one
to avoid the complicated use of Acc/inject/raise when proving
inductive properties over finite sets.

The release candidate can be downloaded here
<https://github.com/agda/agda-stdlib/archive/v1.7-rc1.zip>. We would
be grateful for reports of any issues you may encounter with the new
version of the library on the Github issues page
<https://github.com/agda/agda-stdlib/issues>.

If no major issues are found we will aim to release the official
version 1.7 soon after the release of Agda 2.6.2.

Best wishes,

Matthew, on behalf of the Agda Team
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210527/5ed7d985/attachment.html>


More information about the Agda mailing list