[Agda] ANNOUNCE: Standard library 0.9

[Sergei Meshveliani]

1) I see the renaming   Data.Fin.Props --> Data.Fin.Properties.

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.

Anyway, it seems to type-check the 0.9 library with  Agda-2.4.2.1.

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. I shall
try to fix.

Thanks for release,

------
Sergei


 


On Fri, 2014-11-14 at 19:23 -0500, Andrés Sicard-Ramírez wrote:
> Hi,
> 
> The standard library 0.9 has been released (see
> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary).
> 
> The library has been tested using Agda 2.4.2.1.
> 
> Important changes since 0.8.1:
> https://github.com/agda/agda-stdlib/blob/v0.9/CHANGELOG.
> 
> Note that no guarantees are made about backwards or forwards
> compatibility, the library is still at an experimental stage.
> 
> If you want to compile the library using the MAlonzo compiler, then
> you should first install some supporting Haskell code, for instance as
> follows:
> 
>   cd ffi
>   cabal install
> 
> Currently the library does not support the Epic or JavaScript compiler
> backends.
> 
> 
> -- 
> Andrés, on behalf of the standard library team
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda