[Agda] how to run helloworld in agda

[Andreas Abel]

You need to provide an include path for the standard library.

   agda --interactive -i. -i <PATH-OF-STD-LIB> ag.agda

Cheers,
Andreas

On 08.12.2015 09:10, Mandy Martino wrote:
> The interactive mode is no longer supported. Don't complain if it
> doesn't work.
> Main> :l ag.agda
> Checking ag (/home/martin/adga2/ag.agda).
> /home/martin/adga2/ag.agda:3,13-25
> Failed to find source of module IO.Primitive in any of the
> following 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.lagda
> when scope checking the declaration
> open import IO.Primitive using (IO; putStrLn)
> Failed.
> Main>
>
> module ag where
>
> open import IO.Primitive using (IO; putStrLn)
> open import Data.String using (toCostring; String)
> open import Foreign.Haskell using (Unit)
>
> main : IO Unit
> main = putStrLn (toCostring "Hello, Agda!")
>
>
> after install tar from wiki and install std-lib, confused about this
> example,
>
> why use open import, but not import
>
> which syntax is correct?
>
>
> Regards,
>
>
> Martin
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/