[Agda] how to include Data.List without conflict with agda-prelude

[Ulf Norell]

That example is using the standard library, and not the agda-prelude.

/ Ulf

On Sat, Jan 2, 2016 at 2:55 AM, Mandy Martino <tesleft at hotmail.com> wrote:

> 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-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/20160102/799d9d8d/attachment-0001.html