<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 Ulf,</font><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><font size="3" style="font-size:12pt;" color="#000000">it has error in emacs, even if i include </font>/home/martin/hilbertreborn/agda-stdlib-0.11/ffi</div><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><font color="#000000"><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></font><br><br><div>Regards,</div><div><br></div><div>Martin </div><br><br><div><hr id="stopSpelling">From: ulf.norell@gmail.com<br>Date: Sat, 2 Jan 2016 10:19:40 +0100<br>Subject: Re: [Agda] how to include Data.List without conflict with agda-prelude<br>To: tesleft@hotmail.com<br>CC: asr@eafit.edu.co; agda@lists.chalmers.se<br><br><div dir="ltr">That example is using the standard library, and not the agda-prelude.<div><br></div><div>/ Ulf</div></div><div class="ecxgmail_extra"><br><div class="ecxgmail_quote">On Sat, Jan 2, 2016 at 2:55 AM, Mandy Martino <span dir="ltr"><<a href="mailto:tesleft@hotmail.com" target="_blank">tesleft@hotmail.com</a>></span> wrote:<br><blockquote class="ecxgmail_quote" style="border-left:1px #ccc solid;padding-left:1ex;">
<div><div dir="ltr"><font size="3" style="font-size:12pt;" color="#000000">Hi Ulf,</font><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><font size="3" style="font-size:12pt;" color="#000000">someone replied with this solution, seems he can compile this example, so , how to compile this?</font></div><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><font size="3" style="font-size:12pt;" color="#000000">i include both prelude src directory and stdlib src directory, got conflict, if delete one of them, will have another error. </font></div><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><a href="http://stackoverflow.com/questions/29216463/an-example-on-how-to-use-agda-standard-library-monoid-solver" target="_blank">http://stackoverflow.com/questions/29216463/an-example-on-how-to-use-agda-standard-library-monoid-solver</a></div><div><br><div>Regards,</div><div><br></div><div>Martin </div><br><div class="ecxhm ecxHOEnZb"><br></div><div><div class="ecxhm ecxHOEnZb"><hr>From: <a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a><br>Date: Fri, 1 Jan 2016 11:30:19 +0100<br>Subject: Re: [Agda] how to include Data.List without conflict with agda-prelude<br>To: <a href="mailto:tesleft@hotmail.com" target="_blank">tesleft@hotmail.com</a><br>CC: <a href="mailto:asr@eafit.edu.co" target="_blank">asr@eafit.edu.co</a>; <a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a></div><div><div class="h5"><br><br><div dir="ltr">Unfortunately the standard library and the agda prelude are incompatible since they both define built-in types such as lists.<div><br></div><div>/ Ulf</div></div><div><br><div>On Fri, Jan 1, 2016 at 7:53 AM, Mandy Martino <span dir="ltr"><<a href="mailto:tesleft@hotmail.com" target="_blank">tesleft@hotmail.com</a>></span> wrote:<br><blockquote style="border-left:1px #ccc solid;padding-left:1ex;">
<div><div dir="ltr"><div><div dir="ltr"><div><div>Hi ,</div></div><div><br></div><div>how to include Data.List without conflict with agda-prelude?</div><div><br></div><div><div>/home/martin/hilbertreborn/moso.agda:2,13-22</div><div>Ambiguous module name. The module name Data.List could refer to any</div><div>of the following files:</div><div> /home/martin/hilbertreborn/agda-prelude/src/Data/List.agda</div><div> /home/martin/hilbertreborn/agda-stdlib-0.11/src/Data/List.agda</div><div>when scope checking the declaration</div><div> open import Data.List</div></div><div><br></div><div>Regards,</div><div><br></div><div>Martin</div> </div></div> </div></div>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div></div></div></div></div> </div></div>
</blockquote></div><br></div></div></div> </div></body>
</html>