<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<div>Is it possible to run in interactive mode?<br>
<br>
<div class="acompli_signature">Sent from <a href="https://aka.ms/sdimjr">Outlook Mobile</a></div>
<br>
</div>
<br>
<br>
<br>
<div class="gmail_quote">On Tue, Dec 8, 2015 at 9:08 AM -0800, "Sergei Meshveliani"
<span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br>
<br>
</div>
<div class="BodyFragment">
<div class="PlainText">On Tue, 2015-12-08 at 16:10 +0800, Mandy Martino wrote:<br>
> The interactive mode is no longer supported. Don't complain if it<br>
> doesn't work.<br>
> Main> :l ag.agda<br>
> Checking ag (/home/martin/adga2/ag.agda).<br>
> /home/martin/adga2/ag.agda:3,13-25<br>
> Failed to find source of module IO.Primitive in any of the<br>
> following locations:<br>
> /home/martin/adga2/IO/Primitive.agda<br>
> /home/martin/adga2/IO/Primitive.lagda<br>
> /home/martin/.cabal/share/i386-linux-ghc-7.10.1/Agda-2.4.2.3/lib/prim/IO/Primitive.agda<br>
> /home/martin/.cabal/share/i386-linux-ghc-7.10.1/Agda-2.4.2.3/lib/prim/IO/Primitive.lagda<br>
> when scope checking the declaration<br>
> open import IO.Primitive using (IO; putStrLn)<br>
> Failed.<br>
> Main><br>
> <br>
> module ag where<br>
> <br>
> open import IO.Primitive using (IO; putStrLn)<br>
> open import Data.String using (toCostring; String)<br>
> open import Foreign.Haskell using (Unit)<br>
> <br>
> main : IO Unit<br>
> main = putStrLn (toCostring "Hello, Agda!")<br>
> <br>
<br>
I remove "module ag where" (because this module has `main' in it),<br>
and apply<br>
<br>
agda -c $agdaLibOpt Hello.agda<br>
<br>
where $agdaLibOpt contains the path to the /src directory of<br>
Standard library.<br>
This makes the executable file Hello.<br>
Then, the command <br>
<br>
./Hello <br>
prints <br>
"Hello, Agda!"<br>
<br>
<br>
> why use open import, but not import<br>
<br>
After "import Foo",<br>
<br>
one can write Foo.foo, if foo is defined in Foo module.<br>
After<br>
import Foo<br>
open Foo using (foo) <br>
<br>
one can write `foo' in the scope.<br>
And the line<br>
<br>
open import Foo using (foo)<br>
<br>
combines the above lines of `import' and `open'.<br>
<br>
Regards,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
<br>
</div>
</div>
</body>
</html>