<html>
<head>
<style><!--
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 12pt;
font-family:新細明體
}
--></style></head>
<body class='hmmessage'><div dir='ltr'><p style="box-sizing: border-box; margin-bottom: 16px; color: rgb(51, 51, 51); font-family: 'Helvetica Neue', Helvetica, 'Segoe UI', Arial, freesans, sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', 'Segoe UI Symbol'; font-size: 14px; line-height: 22.4px; background-color: rgb(255, 255, 255);">The interactive mode is no longer supported. Don't complain if it doesn't work.<br style="box-sizing: border-box;">Main> :l ag.agda<br style="box-sizing: border-box;">Checking ag (/home/martin/adga2/ag.agda).<br style="box-sizing: border-box;">/home/martin/adga2/ag.agda:3,13-25<br style="box-sizing: border-box;">Failed to find source of module IO.Primitive in any of the<br style="box-sizing: border-box;">following locations:<br style="box-sizing: border-box;">/home/martin/adga2/IO/Primitive.agda<br style="box-sizing: border-box;">/home/martin/adga2/IO/Primitive.lagda<br style="box-sizing: border-box;">/home/martin/.cabal/share/i386-linux-ghc-7.10.1/Agda-2.4.2.3/lib/prim/IO/Primitive.agda<br style="box-sizing: border-box;">/home/martin/.cabal/share/i386-linux-ghc-7.10.1/Agda-2.4.2.3/lib/prim/IO/Primitive.lagda<br style="box-sizing: border-box;">when scope checking the declaration<br style="box-sizing: border-box;">open import IO.Primitive using (IO; putStrLn)<br style="box-sizing: border-box;">Failed.<br style="box-sizing: border-box;">Main></p><p style="box-sizing: border-box; margin-bottom: 16px; color: rgb(51, 51, 51); font-family: 'Helvetica Neue', Helvetica, 'Segoe UI', Arial, freesans, sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', 'Segoe UI Symbol'; font-size: 14px; line-height: 22.4px; background-color: rgb(255, 255, 255);">module ag where</p><p style="box-sizing: border-box; margin-bottom: 16px; color: rgb(51, 51, 51); font-family: 'Helvetica Neue', Helvetica, 'Segoe UI', Arial, freesans, sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', 'Segoe UI Symbol'; font-size: 14px; line-height: 22.4px; background-color: rgb(255, 255, 255);">open import IO.Primitive using (IO; putStrLn)<br style="box-sizing: border-box;">open import Data.String using (toCostring; String)<br style="box-sizing: border-box;">open import Foreign.Haskell using (Unit)</p><p style="box-sizing: border-box; margin-bottom: 16px; color: rgb(51, 51, 51); font-family: 'Helvetica Neue', Helvetica, 'Segoe UI', Arial, freesans, sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', 'Segoe UI Symbol'; font-size: 14px; line-height: 22.4px; background-color: rgb(255, 255, 255);">main : IO Unit<br style="box-sizing: border-box;">main = putStrLn (toCostring "Hello, Agda!")</p><p style="box-sizing: border-box; margin-bottom: 16px; color: rgb(51, 51, 51); font-family: 'Helvetica Neue', Helvetica, 'Segoe UI', Arial, freesans, sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', 'Segoe UI Symbol'; font-size: 14px; line-height: 22.4px; background-color: rgb(255, 255, 255);"><br></p><p style="box-sizing: border-box; margin-bottom: 16px; color: rgb(51, 51, 51); font-family: 'Helvetica Neue', Helvetica, 'Segoe UI', Arial, freesans, sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', 'Segoe UI Symbol'; font-size: 14px; line-height: 22.4px; background-color: rgb(255, 255, 255);">after install tar from wiki and install std-lib, confused about this example,</p><p style="box-sizing: border-box; margin-bottom: 16px; color: rgb(51, 51, 51); font-family: 'Helvetica Neue', Helvetica, 'Segoe UI', Arial, freesans, sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', 'Segoe UI Symbol'; font-size: 14px; line-height: 22.4px; background-color: rgb(255, 255, 255);">why use open import, but not import</p><p style="box-sizing: border-box; color: rgb(51, 51, 51); font-family: 'Helvetica Neue', Helvetica, 'Segoe UI', Arial, freesans, sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', 'Segoe UI Symbol'; font-size: 14px; line-height: 22.4px; background-color: rgb(255, 255, 255);">which syntax is correct?</p><p style="box-sizing: border-box; color: rgb(51, 51, 51); font-family: 'Helvetica Neue', Helvetica, 'Segoe UI', Arial, freesans, sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', 'Segoe UI Symbol'; font-size: 14px; line-height: 22.4px; background-color: rgb(255, 255, 255);"><br></p><p style="box-sizing: border-box; color: rgb(51, 51, 51); font-family: 'Helvetica Neue', Helvetica, 'Segoe UI', Arial, freesans, sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', 'Segoe UI Symbol'; font-size: 14px; line-height: 22.4px; background-color: rgb(255, 255, 255);">Regards,</p><p style="box-sizing: border-box; color: rgb(51, 51, 51); font-family: 'Helvetica Neue', Helvetica, 'Segoe UI', Arial, freesans, sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', 'Segoe UI Symbol'; font-size: 14px; line-height: 22.4px; background-color: rgb(255, 255, 255);"><br></p><p style="box-sizing: border-box; color: rgb(51, 51, 51); font-family: 'Helvetica Neue', Helvetica, 'Segoe UI', Arial, freesans, sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', 'Segoe UI Symbol'; font-size: 14px; line-height: 22.4px; background-color: rgb(255, 255, 255);">Martin</p><div><div dir="ltr"> </div></div><style><!--
.ExternalClass .ecxhmmessage P {
padding:0px;
}
.ExternalClass body.ecxhmmessage {
font-size:12pt;
font-family:新細明體;
}
--></style> </div></body>
</html>