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

[Mandy Martino]

Hi  Ulf,
it  has  error in emacs, even if  i include  /home/martin/hilbertreborn/agda-stdlib-0.11/ffi
MAlonzo/Code/Agda/Primitive.hs:4:18:    Could not find module `Agda.FFI'    Use -v to see a list of the files searched for.

Regards,
Martin 

From: ulf.norell at gmail.com
Date: Sat, 2 Jan 2016 10:19:40 +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

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-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/60860707/attachment.html