[Agda] how to include Data.List without conflict with agda-prelude
Ulf Norell
ulf.norell at gmail.com
Fri Jan 1 11:30:19 CET 2016
Unfortunately the standard library and the agda prelude are incompatible
since they both define built-in types such as lists.
/ Ulf
On Fri, Jan 1, 2016 at 7:53 AM, Mandy Martino <tesleft at hotmail.com> wrote:
> Hi ,
>
> how to include Data.List without conflict with agda-prelude?
>
> /home/martin/hilbertreborn/moso.agda:2,13-22
> Ambiguous module name. The module name Data.List could refer to any
> of the following files:
> /home/martin/hilbertreborn/agda-prelude/src/Data/List.agda
> /home/martin/hilbertreborn/agda-stdlib-0.11/src/Data/List.agda
> when scope checking the declaration
> open import Data.List
>
> Regards,
>
> Martin
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160101/e9322644/attachment.html
More information about the Agda
mailing list