<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On 15 November 2014 11:35, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div id=":sn" class="" style="overflow:hidden">2) I tries to read about the changes, but the reference<br>
<a href="https://github.com/agda/agda-stdlib/blob/v0.9/CHANGELOG" target="_blank">https://github.com/agda/agda-stdlib/blob/v0.9/CHANGELOG</a>.<br>
<br>
fails to load the page when I click at it.<br>
<br></div></blockquote><div><br></div><div>It works for me.<br></div><div><br> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div id=":sn" class="" style="overflow:hidden">
<br>
Then, I type-check my application, and Agda reports<br>
<br>
---------<br>
/home/mechvel/doconA/0.03/source/List2.agda:697,33-43<br>
Cannot `with` on variable x∈y:del-xs bound in a module telescope<br>
(or patterns of a parent clause)<br>
when inferring the type of x∈y:del-xs<br>
---------<br>
<br>
This is, probably, due to the announced change in the language.</div></blockquote><div><br></div><div>Yes, it is. See issue 1342 (<a href="https://code.google.com/p/agda/issues/detail?id=1342">https://code.google.com/p/agda/issues/detail?id=1342</a>). The CHANGELOG related to this issue is <a href="https://github.com/agda/agda/commit/2f0ee51c4672b73ab52c624da745b22e2b4eda27">https://github.com/agda/agda/commit/2f0ee51c4672b73ab52c624da745b22e2b4eda27</a>. </div><div> </div></div>-- <br><div class="gmail_signature"><div dir="ltr">Andrés<br></div></div>
</div></div>