[Agda] import behavior

Discussion:

Sergei Meshveliani

2018-09-17 13:12:01 UTC

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

Matthew Daggitt

2018-09-17 13:47:36 UTC

Permalink

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.

Post by Sergei Meshveliani
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
Data.List.All.universal
Is this a bug in Agda ?
Regards,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

Matthew Daggitt

2018-09-17 13:50:38 UTC

Permalink

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.

Post by 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.