[Agda] import behavior

[Matthew Daggitt]

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.

On Mon, Sep 17, 2018 at 2:41 PM Sergei Meshveliani <mechvel at botik.ru> wrote:

> Dear all,
>
> I have the code of kind
>
> --------------------------
> open import Data.List.All as AllM using (All)
> ...
>   ...
>   all1 :  All foo mons
>   all1 =  AllM.universal mon*zeroPol mons               -- (I)
>           -- Data.List.All.universal mon*zeroPol mons   -- (II)
> --------------------------
>
> The line (I) is type-checked in Agda 2.6.0-05e8112,
> and for the line (II) it is reported
>
>   Not in scope:
>     Data.List.All.universal
>
> Is this a bug in Agda ?
>
> Regards,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180917/fe83aec1/attachment.html>