<html>
<head>
<style><!--
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 12pt;
font-family:新細明體
}
--></style></head>
<body class='hmmessage'><div dir='ltr'><font size="3" style="font-size:12pt;" color="#000000">Hi Andres,</font><div><br></div><div><span style="font-size: 12pt;">After meet message need {-# BUILTIN IO name #-},</span></div><div><span style="font-size: 12pt;"><br></span></div><div><span style="font-size: 12pt;">i add </span><span style="font-size: 12pt;">{-# BUILTIN IO name #-} or </span><span style="font-size: 12pt;">{-# BUILTIN IO hello #-}, still have error,</span></div><div><span style="font-size: 12pt;"><br></span></div><div><span style="font-size: 12pt;">when and where need this?</span></div><div><br></div><div><div>martin@ubuntu:~/hilbertreborn$ time agda -c hello.agda -i. -iagda-stdlib-0.11/src --ghc-flag=/home/martin/hilbertreborn/agda-prelude/agda-ffi/Agda/FFI.hs</div><div>Checking hello (/home/martin/hilbertreborn/hello.agda).</div><div>/home/martin/hilbertreborn/hello.agda:1,16-20</div><div>Not in scope:</div><div> name at /home/martin/hilbertreborn/hello.agda:1,16-20</div><div>when scope checking name</div><div><br></div><div>real<span class="Apple-tab-span" style="white-space:pre"> </span>0m0.080s</div><div>user<span class="Apple-tab-span" style="white-space:pre"> </span>0m0.012s</div><div>sys<span class="Apple-tab-span" style="white-space:pre"> </span>0m0.024s</div><div>martin@ubuntu:~/hilbertreborn$ cat hello.agda</div><div>{-# BUILTIN IO name #-}</div><div>open import Data.Nat.Base</div><div>open import Relation.Binary.PropositionalEquality</div><div>open import Algebra.Structures as A using (IsCommutativeMonoid)</div><div>open import Data.Nat.Properties using (isCommutativeSemiring)</div><div><br></div><div>open A.IsCommutativeSemiring</div><div>open A.IsCommutativeMonoid (+-isCommutativeMonoid isCommutativeSemiring)</div><div><br></div><div>ex : ∀ n → (n + 1) + 1 ≡ n + 2</div><div>ex n = assoc n 1 1</div><div><br></div><div>main : IO Unit</div><div>main = ex</div></div><div><br></div><div><br></div><div><div>Compiling Relation.Binary.Reflection in /home/martin/hilbertreborn/agda-stdlib-0.11/src/Relation/Binary/Reflection.agdai to /home/martin/hilbertreborn/MAlonzo/Code/Relation/Binary/Reflection.hs</div><div>Relation.Nullary : no compilation is needed.</div><div>Compiling Relation.Nullary.Decidable in /home/martin/hilbertreborn/agda-stdlib-0.11/src/Relation/Nullary/Decidable.agdai to /home/martin/hilbertreborn/MAlonzo/Code/Relation/Nullary/Decidable.hs</div><div>Compiling hello in /home/martin/hilbertreborn/hello.agdai to /home/martin/hilbertreborn/MAlonzo/Code/Qhello.hs</div><div>No binding for builtin thing IO, use {-# BUILTIN IO name #-} to</div><div>bind it to 'name'</div><div><br></div><div>real<span class="Apple-tab-span" style="white-space:pre"> </span>0m11.462s</div><div>user<span class="Apple-tab-span" style="white-space:pre"> </span>0m5.528s</div><div>sys<span class="Apple-tab-span" style="white-space:pre"> </span>0m4.080s</div><div><br></div><br><div>Regards,</div><div><br></div><div>Martin </div><br><br><div>> From: asr@eafit.edu.co<br>> Date: Sat, 19 Dec 2015 07:28:33 -0500<br>> Subject: Re: [Agda] how to run helloworld in agda<br>> To: tesleft@hotmail.com<br>> CC: agda@lists.chalmers.se<br>> <br>> On 19 December 2015 at 07:01, Mandy Martino <tesleft@hotmail.com> wrote:<br>> > succeed to run an example, but got error + not in scope when follow a<br>> > web site,<br>> ><br>> > open import Algebra.Structures as A using (IsCommutativeMonoid)<br>> > open import Data.Nat.Properties using (isCommutativeSemiring)<br>> ><br>> <br>> Missing modules:<br>> <br>> open import Data.Nat.Base<br>> open import Relation.Binary.PropositionalEquality<br>> <br>> Please report this error to the author of the Agda tutorial.<br>> <br>> -- <br>> Andrés<br></div></div> </div></body>
</html>