<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><div style="line-height: 21.3px; color: rgb(68, 68, 68); font-size: 15px; background-color: rgb(255, 255, 255);"><br style="line-height: 21.3px;"></div><div style="line-height: 21.3px; color: rgb(68, 68, 68); font-size: 15px; background-color: rgb(255, 255, 255);">i succeed to run an example, but got error + not in scope when follow a web site, </div><div style="line-height: 21.3px; color: rgb(68, 68, 68); font-size: 15px; background-color: rgb(255, 255, 255);">Any more need to import or what syntax is error ?</div><div style="line-height: 21.3px; color: rgb(68, 68, 68); font-size: 15px; background-color: rgb(255, 255, 255);"><br style="line-height: 21.3px;"></div><div style="line-height: 21.3px; color: rgb(68, 68, 68); font-size: 15px; background-color: rgb(255, 255, 255);"><div style="line-height: 21.3px;">/home/martin/hilbertreborn/hello.agda:7,15-16</div><div style="line-height: 21.3px;">Not in scope:</div><div style="line-height: 21.3px;"> + at /home/martin/hilbertreborn/hello.agda:7,15-16</div><div style="line-height: 21.3px;">when scope checking +</div><div style="line-height: 21.3px;"><br style="line-height: 21.3px;"></div><div style="line-height: 21.3px;">real<span class="ecxApple-tab-span" style="line-height: 21.3px; white-space: pre;"> </span>0m3.857s</div><div style="line-height: 21.3px;">user<span class="ecxApple-tab-span" style="line-height: 21.3px; white-space: pre;"> </span>0m2.056s</div><div style="line-height: 21.3px;">sys<span class="ecxApple-tab-span" style="line-height: 21.3px; white-space: pre;"> </span>0m0.856s</div><div style="line-height: 21.3px;"><br style="line-height: 21.3px;"></div><div style="line-height: 21.3px;"><font color="#000000" style="line-height: normal;"><div style="line-height: 21.3px;">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 style="line-height: 21.3px;"><br style="line-height: 21.3px;"></div><div style="line-height: 21.3px;">open import Algebra.Structures as A using (IsCommutativeMonoid)</div><div style="line-height: 21.3px;">open import Data.Nat.Properties using (isCommutativeSemiring)</div><div style="line-height: 21.3px;"><br style="line-height: 21.3px;"></div><div style="line-height: 21.3px;">open A.IsCommutativeSemiring</div><div style="line-height: 21.3px;">open A.IsCommutativeMonoid (+-isCommutativeMonoid isCommutativeSemiring)</div><div style="line-height: 21.3px;"><br style="line-height: 21.3px;"></div><div style="line-height: 21.3px;">ex : ∀ n → (n + 1) + 1 ≡ n + 2</div><div style="line-height: 21.3px;">ex n = assoc n 1 1</div><div style="line-height: 21.3px;"><br style="line-height: 21.3px;"></div><div style="line-height: 21.3px;">main = ex</div></font></div><div style="line-height: 21.3px;"><font color="#000000" style="line-height: normal; font-size: 12pt;"><br id="ecxFontBreak" style="line-height: 22.72px;"></font><br style="line-height: 21.3px;"><div style="line-height: 21.3px;"><a href="http://people.inf.elte.hu/divip/AgdaTutorial/Application.Algebra.html" target="" style="line-height: 21.3px; font-weight: inherit; color: rgb(0, 104, 207); cursor: pointer;">http://people.inf.elte.hu/divip/AgdaTutorial/Application.Algebra.html</a></div><div style="line-height: 21.3px;"><br style="line-height: 21.3px;"></div><div style="line-height: 21.3px;"><br style="line-height: 21.3px;"></div><div style="line-height: 21.3px;">Regards,</div><div style="line-height: 21.3px;"><br style="line-height: 21.3px;"></div><div style="line-height: 21.3px;">Martin </div></div></div><br><div>> From: asr@eafit.edu.co<br>> Date: Sat, 19 Dec 2015 06:43:14 -0500<br>> Subject: Re: [Agda] how to run helloworld in agda<br>> To: tesleft@hotmail.com<br>> <br>> Hi Mandy,<br>> <br>> Please resend the question to Agda users mailing list.<br>> <br>> Best.<br>> <br>> <br>> On 19 December 2015 at 06:27, Mandy Martino <tesleft@hotmail.com> wrote:<br>> > Hi,<br>> ><br>> > i succeed to run an example, but got error + not in scope when follow<br>> > a web site,<br>> > Any more need to import or what syntax is error ?<br>> ><br>> > /home/martin/hilbertreborn/hello.agda:7,15-16<br>> > Not in scope:<br>> > + at /home/martin/hilbertreborn/hello.agda:7,15-16<br>> > when scope checking +<br>> ><br>> > real 0m3.857s<br>> > user 0m2.056s<br>> > sys 0m0.856s<br>> ><br>> > time agda -c hello.agda -i. -iagda-stdlib-0.11/src<br>> > --ghc-flag=/home/martin/hilbertreborn/agda-prelude/agda-ffi/Agda/FFI.hs<br>> ><br>> > open import Algebra.Structures as A using (IsCommutativeMonoid)<br>> > open import Data.Nat.Properties using (isCommutativeSemiring)<br>> ><br>> > open A.IsCommutativeSemiring<br>> > open A.IsCommutativeMonoid (+-isCommutativeMonoid isCommutativeSemiring)<br>> ><br>> > ex : ∀ n → (n + 1) + 1 ≡ n + 2<br>> > ex n = assoc n 1 1<br>> ><br>> > main = ex<br>> ><br>> ><br>> > http://people.inf.elte.hu/divip/AgdaTutorial/Application.Algebra.html<br>> ><br>> ><br>> > Regards,<br>> ><br>> > Martin<br>> ><br>> ><br>> >> From: asr@eafit.edu.co<br>> >> Date: Sat, 19 Dec 2015 05:46:11 -0500<br>> >> Subject: Re: [Agda] how to run helloworld in agda<br>> >> To: tesleft@hotmail.com<br>> >><br>> >> On 19 December 2015 at 05:39, Mandy Martino <tesleft@hotmail.com> wrote:<br>> >> > MAlonzo/Code/Agda/Primitive.hs:4:18:<br>> >> > Could not find module `Agda.FFI'<br>> >> > Use -v to see a list of the files searched for.<br>> >><br>> >> From agda-stdlib README.agda:<br>> >><br>> >> -- To compile the library using the MAlonzo compiler you first need to<br>> >> -- install some supporting Haskell code, for instance as follows:<br>> >> --<br>> >> -- cd ffi<br>> >> -- cabal install<br>> >><br>> >><br>> >> --<br>> >> Andrés<br>> ><br>> ><br>> > "La información contenida en este correo electrónico está dirigida<br>> > únicamente a su destinatario y puede contener información confidencial,<br>> > material privilegiado o información protegida por derecho de autor. Está<br>> > prohibida cualquier copia, utilización, indebida retención, modificación,<br>> > difusión, distribución o reproducción total o parcial. Si usted recibe este<br>> > mensaje por error, por favor contacte al remitente y elimínelo. La<br>> > información aquí contenida es responsabilidad exclusiva de su remitente por<br>> > lo tanto la Universidad EAFIT no se hace responsable de lo que el mensaje<br>> > contenga."<br>> ><br>> > "The information contained in this email is addressed to its recipient only<br>> > and may contain confidential information, privileged material or information<br>> > protected by copyright. Its prohibited any copy, use, improper retention,<br>> > modification, dissemination, distribution or total or partial reproduction.<br>> > If you receive this message by error, please contact the sender and delete<br>> > it. The information contained herein is the sole responsibility of the<br>> > sender therefore Universidad EAFIT is not responsible for what the message<br>> > contains."<br>> <br>> <br>> <br>> -- <br>> Andrés<br></div></div> </div></body>
</html>