[Agda] how to include Data.List without conflict with agda-prelude
Mandy Martino
tesleft at hotmail.com
Sat Jan 2 02:55:16 CET 2016
Hi Ulf,
someone replied with this solution, seems he can compile this example, so , how to compile this?
i include both prelude src directory and stdlib src directory, got conflict, if delete one of them, will have another error.
http://stackoverflow.com/questions/29216463/an-example-on-how-to-use-agda-standard-library-monoid-solver
Regards,
Martin
From: ulf.norell at gmail.com
Date: Fri, 1 Jan 2016 11:30:19 +0100
Subject: Re: [Agda] how to include Data.List without conflict with agda-prelude
To: tesleft at hotmail.com
CC: asr at eafit.edu.co; agda at lists.chalmers.se
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-22Ambiguous module name. The module name Data.List could refer to anyof the following files: /home/martin/hilbertreborn/agda-prelude/src/Data/List.agda /home/martin/hilbertreborn/agda-stdlib-0.11/src/Data/List.agdawhen 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/20160102/ba8f5e3b/attachment-0001.html
More information about the Agda
mailing list