[Agda] [ ANNOUNCE ] Standard library version 1.7

Matthew Daggitt matthewdaggitt at gmail.com
Sun Jun 20 09:23:06 CEST 2021


Dear all,
 The Agda Team is pleased to announce the release of version 1.7 of the
standard library. The release has been tested using Agda 2.6.2, and
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 can be downloaded here
<https://github.com/agda/agda-stdlib/archive/v1.7.tar.gz>.
Best wishes,
Matthew, on behalf of the Agda Team
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210620/cc87ed2b/attachment.html>


More information about the Agda mailing list