[Agda] how to run helloworld in agda

[Mandy Martino]

Hi  Andres,
is there an  example to use  function  in Algebra folderand import  Algebra?
 i would like to  test  what is the correct  command  to  compile  example for  std-lib .
Regards,
Martin 

> From: asr at eafit.edu.co
> Date: Sat, 19 Dec 2015 05:04:14 -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:40, Mandy Martino <tesleft at hotmail.com> wrote:
> > time agda -c hello.agda -i. -iagda-prelude/src -iagda-stdlib/src
> > --ghc-flag=agda-prelude/agda-ffi/Agda/FFI.hs
> >
> > got  error  when  run  above  command,  would like to display  some simple
> > result  when  using Algebra  library in stdlibrary,
> 
> By removing `-iagda-stdlib/src` in the above command, you can run the
> hello program:
> 
>   $ time agda -c hello.agda -i. -iagda-prelude/src
> --ghc-flag=agda-prelude/agda-ffi/Agda/FFI.hs
>   $ ./hello
>   Hello World
> 
> -- 
> Andrés
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151219/424d3d78/attachment.html