[Agda] lib for Development Agda

Guillaume Allais guillaume.allais at ens-lyon.org
Tue Nov 6 18:46:37 CET 2018


Hi Sergei,

`Data.List.Relation.Sublist.Extensional.Setoid` has been moved
to `Data.List.Relation.Subset.Setoid` because it was not define
a sublist relation but rather a subset one.

All of the breaking and non-breaking changes are documented in
the CHANGELOG for the standard library to make migration as
smooth as possible:
https://github.com/agda/agda-stdlib/blob/master/CHANGELOG/v0.17.md

Best,
--
gallais

On 06/11/18 12:56, Sergei Meshveliani wrote:
> Dear Agda team,
> 
> Is is true that Development Agda of November 6 2018 
> (2.6.0-e7da0ce)
> uses Standard library  lib-0.17 ?
> 
> I try to upgrade the application from Development Agda of September 7 to
> Development of November 6,
> and it reports
>   Failed to find source of module
>   Data.List.Relation.Sublist.Extensional.Setoid in any of the
>   following locations:
>   ...
> 
> It is desirable to understand what is the intended library for the
> official Agda version to which Development Agda approaches. 
> 
> Regards,
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181106/50b4eb86/attachment.sig>


More information about the Agda mailing list