<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><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><font size="3" style="font-size:12pt;" color="#000000">i use only one line import Algebra and then compile got error</font></div><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><font color="#000000"><div>martin@ubuntu:~/hilbertreborn$ cat hello.agda</div><div>open import Algebra</div><div>martin@ubuntu:~/hilbertreborn$</div><div><br></div><div>martin@ubuntu:~/hilbertreborn$ time agda -c hello.agda -i. -iagda-stdlib-0.11/src --ghc-flag=/home/martin/hilbertreborn/agda-stdlib-0.11/ffi/Data/FFI.hs</div><div><br></div></font><div><span style="font-size: 12pt;">/home/martin/hilbertreborn/MAlonzo/Code/Relation/Binary/PropositionalEquality/Core.hs</span></div><div>Compiling Relation.Nullary in /home/martin/hilbertreborn/agda-stdlib-0.11/src/Relation/Nullary.agdai to /home/martin/hilbertreborn/MAlonzo/Code/Relation/Nullary.hs</div><div>Compiling hello in /home/martin/hilbertreborn/hello.agdai to /home/martin/hilbertreborn/MAlonzo/Code/Qhello.hs</div><div>Calling: ghc -O -o /home/martin/hilbertreborn/hello -Werror /home/martin/hilbertreborn/agda-stdlib-0.11/ffi/Data/FFI.hs -i/home/martin/hilbertreborn -main-is MAlonzo.Code.Qhello /home/martin/hilbertreborn/MAlonzo/Code/Qhello.hs --make -fwarn-incomplete-patterns -fno-warn-overlapping-patterns</div><div>Compilation error:</div><div><br></div><div>MAlonzo/Code/Agda/Primitive.hs:4:18:</div><div> Could not find module `Agda.FFI'</div><div> Use -v to see a list of the files searched for.</div><div><br></div><div><br></div><div>real<span class="Apple-tab-span" style="white-space:pre"> </span>0m9.028s</div><div>user<span class="Apple-tab-span" style="white-space:pre"> </span>0m6.140s</div><div>sys<span class="Apple-tab-span" style="white-space:pre"> </span>0m1.436s</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 05:29:42 -0500<br>> Subject: Re: [Agda] how to run helloworld in agda<br>> To: tesleft@hotmail.com<br>> CC: leo@halfaya.org; ulf.norell@gmail.com; agda@lists.chalmers.se<br>> <br>> On 19 December 2015 at 05:11, Mandy Martino <tesleft@hotmail.com> wrote:<br>> > how to uninstall this incompatible version?<br>> <br>> There is no command for uninstalling the agda-stdlib library. You can<br>> delete the agda-stdlib directory or you can use a different directory<br>> for a different version of the agda-stdlib library.<br>> <br>> <br>> -- <br>> Andrés<br></div></div> </div></body>
</html>