[Agda] how to run helloworld in agda

[Andrés Sicard-Ramírez]

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