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

Mandy Martino tesleft at hotmail.com
Sun Jan 3 07:23:20 CET 2016


Hi  Andres,
actually  i  followed  this  part many  times,  just  do  not  understand where to type   using the-- --include-path flag.
already  cd   ffi  and cabal install  in  this directory , still  Could not find module `Agda.FFI'
-- To make use of the library, add the path to the library’s root-- directory (src) to the Agda search path, either using the-- --include-path flag or by customising the Emacs mode variable-- agda2-include-dirs (M-x customize-group RET agda2 RET).
-- To compile the library using the MAlonzo compiler you first need to-- install some supporting Haskell code, for instance as follows:----   cd ffi--   cabal install

Regards,
Martin 

> From: asr at eafit.edu.co
> Date: Sat, 2 Jan 2016 08:20:46 -0500
> Subject: Re: [Agda] how to include Data.List without conflict with agda-prelude
> To: tesleft at hotmail.com
> CC: ulf.norell at gmail.com; agda at lists.chalmers.se
> 
> On 2 January 2016 at 08:01, Mandy Martino <tesleft at hotmail.com> wrote:
> > MAlonzo/Code/Agda/Primitive.hs:4:18:
> >     Could not find module `Agda.FFI'
> >     Use -v to see a list of the files searched for.
> 
> See README.agda from the standard library.
> 
> 
> -- 
> Andrés
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160103/aba95f98/attachment.html


More information about the Agda mailing list