<div dir="ltr">Oh no hang on, that's not what you're asking. My mistake. It's not a bug, you've renamed the module `Data.List.All` as `AllM` so the name `Data.List.All` no longer exists in the namespace. Not a bug, expected behaviour.</div><br><div class="gmail_quote"><div dir="ltr">On Mon, Sep 17, 2018 at 2:47 PM Matthew Daggitt <<a href="mailto:matthewdaggitt@gmail.com">matthewdaggitt@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">There is no `universal` in `Data.List.All` in the current release of the standard library (v0.16). I assume you're looking at the development version of the library in which `universal` has been added.</div><br><div class="gmail_quote"><div dir="ltr">On Mon, Sep 17, 2018 at 2:41 PM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear all,<br>
<br>
I have the code of kind<br>
<br>
--------------------------<br>
open import Data.List.All as AllM using (All)<br>
...<br>
  ...<br>
  all1 :  All foo mons<br>
  all1 =  AllM.universal mon*zeroPol mons               -- (I) <br>
          -- Data.List.All.universal mon*zeroPol mons   -- (II)<br>
--------------------------<br>
<br>
The line (I) is type-checked in Agda 2.6.0-05e8112,<br>
and for the line (II) it is reported<br>
<br>
  Not in scope:<br>
    Data.List.All.universal<br>
<br>
Is this a bug in Agda ?<br>
<br>
Regards,<br>
<br>
------<br>
Sergei<br>
<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>
</blockquote></div>
</blockquote></div>