<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 class="gmail_extra"><br><div class="gmail_quote">On Fri, Jan 1, 2016 at 7:53 AM, Mandy Martino <span dir="ltr">&lt;<a href="mailto:tesleft@hotmail.com" target="_blank">tesleft@hotmail.com</a>&gt;</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"><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">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>