[Agda] ANNOUNCE: Standard library 0.9

[Andrés Sicard-Ramírez]

On 15 November 2014 11:35, Sergei Meshveliani <mechvel at botik.ru> wrote:

> 2) I tries to read about the changes, but the reference
>     https://github.com/agda/agda-stdlib/blob/v0.9/CHANGELOG.
>
> fails to load the page when I click at it.
>
>
It works for me.



>
> Then, I type-check my application, and Agda reports
>
> ---------
> /home/mechvel/doconA/0.03/source/List2.agda:697,33-43
> Cannot `with` on variable x∈y:del-xs bound in a module telescope
> (or patterns of a parent clause)
> when inferring the type of x∈y:del-xs
> ---------
>
> This is, probably, due to the announced change in the language.
>

Yes, it is. See issue 1342 (
https://code.google.com/p/agda/issues/detail?id=1342). The CHANGELOG
related to this issue is
https://github.com/agda/agda/commit/2f0ee51c4672b73ab52c624da745b22e2b4eda27.


-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141115/c25ee7ea/attachment.html