[Agda] import behavior

[Matthew Daggitt]

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.

On Mon, Sep 17, 2018 at 2:47 PM Matthew Daggitt <matthewdaggitt at gmail.com>
wrote:

> 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/8faaea25/attachment.html>