[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