[Agda] how to run helloworld in agda

Andrés Sicard-Ramírez asr at eafit.edu.co
Sat Dec 19 13:07:51 CET 2015


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,

A simple example using IO.Primitive:

  $ cat HelloWorld.agda
  module HelloWorld where

  open import Data.String
  open import Foreign.Haskell
  open import IO.Primitive

  main : IO Unit
  main = putStrLn (toCostring "Hello World!")

  $ agda -c -i. -iagda-stdlib/src HelloWorld.agda
  $ ./HelloWorld
  Hello World!

-- 
Andrés


More information about the Agda mailing list