<div dir="ltr"><p style="margin:0px 0px 10px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">Dear all,<br> 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:</p><ul style="padding:0px;margin:0px 0px 10px 25px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px"><li style="line-height:inherit">New module for making system calls during type checking, Reflection.External, which re-exports Agda.Builtin.Reflection.External.</li><li style="line-height:inherit">New predicate for lists that are enumerations of their type in Data.List.Relation.Unary.Enumerates.</li><li style="line-height:inherit">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.</li></ul><p style="margin:0px 0px 10px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">The release can be downloaded <a href="https://github.com/agda/agda-stdlib/archive/v1.7.tar.gz">here</a>.<br>Best wishes,<br>Matthew, on behalf of the Agda Team</p></div>