<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">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>