<div dir="ltr">That example is using the standard library, and not the agda-prelude.<div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_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="gmail_quote" style="margin:0 0 0 .8ex;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="hm HOEnZb"><br></div><div><div class="hm HOEnZb"><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>