[Agda] how to run helloworld in agda
Sergei Meshveliani
mechvel at botik.ru
Tue Dec 8 18:06:16 CET 2015
On Tue, 2015-12-08 at 16:10 +0800, 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!")
>
I remove "module ag where" (because this module has `main' in it),
and apply
agda -c $agdaLibOpt Hello.agda
where $agdaLibOpt contains the path to the /src directory of
Standard library.
This makes the executable file Hello.
Then, the command
./Hello
prints
"Hello, Agda!"
> why use open import, but not import
After "import Foo",
one can write Foo.foo, if foo is defined in Foo module.
After
import Foo
open Foo using (foo)
one can write `foo' in the scope.
And the line
open import Foo using (foo)
combines the above lines of `import' and `open'.
Regards,
------
Sergei
More information about the Agda
mailing list