<meta http-equiv="Content-Type" content="text/html; charset=utf-8"><div dir="ltr"><div class="gmail_quote"><div dir="ltr"><div style="font-family:arial,helvetica,sans-serif;font-size:small">Dear all,<br>
<br>
The Agda Team is very pleased to <span>announce</span> <span class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">the </span>release of Agda 2.6.2.<br>
</div><div><br></div><div><div style="font-family:arial,helvetica,sans-serif;font-size:small"># Highlights<br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small"></div><div style="font-family:arial,helvetica,sans-serif;font-size:small"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small"><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default">* Several improvements and bug-fixes related to Run-time Irrelevance (<a href="https://agda.readthedocs.io/en/v2.6.2/language/runtime-irrelevance.html">https://agda.readthedocs.io/en/v2.6.2/language/runtime-irrelevance.html</a>).<br><br>* Several improvements and bug-fixes related to the JavaScript Backend (<a href="https://agda.readthedocs.io/en/v2.6.2/tools/compilers.html#javascript-backend">https://agda.readthedocs.io/en/v2.6.2/tools/compilers.html#javascript-backend</a>).<br><br>* Added experimental support for Guarded Cubical Agda (<a href="https://agda.readthedocs.io/en/v2.6.2/language/guarded-cubical.html">https://agda.readthedocs.io/en/v2.6.2/language/guarded-cubical.html</a>).<br><br>* The Primitive Sorts (<a href="https://agda.readthedocs.io/en/v2.6.2/language/built-ins.html#sorts">https://agda.readthedocs.io/en/v2.6.2/language/built-ins.html#sorts</a>) of Agda (`Set` and `Prop`) are no longer keywords and can be renamed when importing `Agda.Primitive`.<br><br>* Added native support for the Inspect Idiom (<a href="https://agda.readthedocs.io/en/v2.6.2/language/with-abstraction.html#with-abstraction-equality">https://agda.readthedocs.io/en/v2.6.2/language/with-abstraction.html#with-abstraction-equality</a>).<br><br>* Added support for making System Calls (<a href="https://agda.readthedocs.io/en/v2.6.2/language/reflection.html#system-calls">https://agda.readthedocs.io/en/v2.6.2/language/reflection.html#system-calls</a>)<br>  from the reflection API.<br></div></div></div><div><div style="font-family:arial,helvetica,sans-serif;font-size:small"># GHC supported versions<br>
<br>
Agda 2.6.2 has been tested with GHC 9.0.1, 8.10.<span class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">5</span>, 8.8.4, 8.6.5, 8.4.4, 8.2.2 and 8.0.2 on Linux, macOS and Windows.</div><div style="font-family:arial,helvetica,sans-serif;font-size:small"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small"># Installation<br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small"><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default">You can install Agda 2.6.2 with Cabal or stack. See <a href="https://agda.readthedocs.io/en/v2.6.2/getting-started/installation.html">https://agda.readthedocs.io/en/v2.6.2/getting-started/installation.html</a> .<br><br></div></div><div style="font-family:arial,helvetica,sans-serif;font-size:small"># Standard library<br><br>
For the time being, you can use the *<span class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">master</span>* branch of the standard library with Agda 2.6.2<span class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small"> </span><span class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">(</span><a href="https://github.com/agda/agda-stdlib/" target="_blank">https://github.com/agda/agda-stdlib/</a><span class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">).</span></div><div style="font-family:arial,helvetica,sans-serif;font-size:small"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small"># Fixed issues</div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default">    <a href="https://hackage.haskell.org/package/Agda-2.6.2/changelog">https://hackage.haskell.org/package/Agda-2.6.2/changelog</a></div></div><div style="font-family:arial,helvetica,sans-serif;font-size:small"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small">Enjoy Agda 2.6.2<span class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small"></span>.</div><div><br><div style="font-family:arial,helvetica,sans-serif;font-size:small"></div>-- <br></div><div dir="ltr" data-smartmail="gmail_signature">Andrés<span class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">,  on behalf of the Agda Team</span></div></div>
</div><br></div>