[Agda] how to run helloworld in agda

[Mandy Martino]

The interactive mode is no longer supported. Don't complain if it doesn't work.Main> :l ag.agdaChecking ag (/home/martin/adga2/ag.agda)./home/martin/adga2/ag.agda:3,13-25Failed to find source of module IO.Primitive in any of thefollowing locations:/home/martin/adga2/IO/Primitive.agda/home/martin/adga2/IO/Primitive.lagda/home/martin/.cabal/share/i386-linux-ghc-7.10.1/Agda-2.4.2.3/lib/prim/IO/Primitive.agda/home/martin/.cabal/share/i386-linux-ghc-7.10.1/Agda-2.4.2.3/lib/prim/IO/Primitive.lagdawhen scope checking the declarationopen import IO.Primitive using (IO; putStrLn)Failed.Main>module ag whereopen import IO.Primitive using (IO; putStrLn)open import Data.String using (toCostring; String)open import Foreign.Haskell using (Unit)main : IO Unitmain = putStrLn (toCostring "Hello, Agda!")
after install tar from wiki and install std-lib, confused about this example,why use open import, but not importwhich syntax is correct?
Regards,
Martin 		 	   		   		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151208/3177ae62/attachment.html