<div dir="ltr"><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><font face="arial, helvetica, sans-serif">Dear all,

The <span class="gmail-il">Agda</span> Team is very pleased to announce the release of the standard
library 1.4. The library has been tested using <span class="gmail-il">Agda</span> 2.6.1.1. and 2.6.1.
</font></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><pre style="white-space:pre-wrap"><font face="arial, helvetica, sans-serif">The new version of the library, CHANGELOG and README are available at</font></pre><font face="arial, helvetica, sans-serif">  <a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary" target="_blank">http://wiki.portal.chalmers.se/<span class="gmail-il">agda</span>/pmwiki.php?n=Libraries.StandardLibrary</a>
</font></pre><pre style="white-space:pre-wrap"><font face="arial, sans-serif" style="color:rgb(0,0,0)">Highlights include:</font><font color="#000000">
</font><font face="arial, sans-serif"><ul><li><font face="arial, sans-serif">First instance modules, which provide <code style="box-sizing:border-box;font-size:13.6px;padding:0.2em 0.4em;margin:0px;background-color:rgba(27,31,35,0.05);border-radius:6px">Functor</code>, <code style="box-sizing:border-box;font-size:13.6px;padding:0.2em 0.4em;margin:0px;background-color:rgba(27,31,35,0.05);border-radius:6px">Monad</code>, <code style="box-sizing:border-box;font-size:13.6px;padding:0.2em 0.4em;margin:0px;background-color:rgba(27,31,35,0.05);border-radius:6px">Applicative</code> instances for various datatypes. Found under <code style="box-sizing:border-box;font-size:13.6px;padding:0.2em 0.4em;margin:0px;background-color:rgba(27,31,35,0.05);border-radius:6px">Data.X.Instances</code>.
</font></li><li><span style="font-family:arial,sans-serif">New standardised numeric predicates </span><code style="box-sizing:border-box;font-size:13.6px;padding:0.2em 0.4em;margin:0px;background-color:rgba(27,31,35,0.05);border-radius:6px">NonZero</code><span style="font-family:arial,sans-serif">, </span><code style="box-sizing:border-box;font-size:13.6px;padding:0.2em 0.4em;margin:0px;background-color:rgba(27,31,35,0.05);border-radius:6px">Positive</code><span style="font-family:arial,sans-serif">, </span><code style="box-sizing:border-box;font-size:13.6px;padding:0.2em 0.4em;margin:0px;background-color:rgba(27,31,35,0.05);border-radius:6px">Negative</code><span style="font-family:arial,sans-serif">, </span><code style="box-sizing:border-box;font-size:13.6px;padding:0.2em 0.4em;margin:0px;background-color:rgba(27,31,35,0.05);border-radius:6px">NonPositive</code><span style="font-family:arial,sans-serif">, </span><code style="box-sizing:border-box;font-size:13.6px;padding:0.2em 0.4em;margin:0px;background-color:rgba(27,31,35,0.05);border-radius:6px">NonNegative</code><span style="font-family:arial,sans-serif">, especially designed to work as instance arguments.
</span></li><li><span style="font-family:arial,sans-serif">A </span>hierarchy<span style="font-family:arial,sans-serif"> of metric spaces and functions, including a specialisation to ℕ.</span></li></ul></font></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><font face="arial, sans-serif">Best wishes,</font></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><font face="arial, sans-serif">Matthew, on behalf of the <span class="gmail-il">Agda</span> Team</font></pre></div>