[Agda] how to run helloworld in agda

[Mandy Martino]

Hi  Andres,
how to uninstall  this  incompatible  version?
Regards,
Martin 

> From: asr at eafit.edu.co
> Date: Sat, 19 Dec 2015 04:57:23 -0500
> Subject: Re: [Agda] how to run helloworld in agda
> To: tesleft at hotmail.com
> CC: leo at halfaya.org; ulf.norell at gmail.com; agda at lists.chalmers.se
> 
> On 19 December 2015 at 03:23, Mandy Martino <tesleft at hotmail.com> wrote:
> > time agda -c hello.agda -i. -iagda-stdlib/src/
> > --ghc-flag=/home/martin/hilbertreborn/agda-stdlib/ffi/IO/FFI.hs
> >
> 
> You don't need `--ghc-flag=/home/martin/hilbertreborn/agda-stdlib/ffi/IO/FFI.hs`
> with the agda-stdlib library.
> 
> 
> > open import IO
> > main = putStrLn "Hello World"
> >
> 
> The above program requires the agda-prelude library, but you are using
> the agda-stdlib library.
> 
> > martin at ubuntu:~/hilbertreborn$ time agda -c hello.agda -i.
> > -iagda-stdlib/src/
> > --ghc-flag=/home/martin/hilbertreborn/agda-stdlib/ffi/IO/FFI.hs
> ...
> > (/home/martin/hilbertreborn/agda-stdlib/src/Data/Maybe/Base.agda).
> >      Checking Data.Bool.Base
> > (/home/martin/hilbertreborn/agda-stdlib/src/Data/Bool/Base.agda).
> > /home/martin/hilbertreborn/agda-stdlib/src/Data/Bool/Base.agda:32,5-5
> > /home/martin/hilbertreborn/agda-stdlib/src/Data/Bool/Base.agda:32,5: Parse
> > error
> > COMPILED_DATA_UHC<ERROR>
> >  Bool __BOOL__ __TRUE__ __FALS...
> 
> Your version of agda-stdlib is not compatible with your version of Agda.
> 
> In http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary
> you can see which version of agda-stdlib is compatible with your
> version of Agda.
> 
> -- 
> Andrés
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151219/ffbee906/attachment.html