[Agda] import behavior
Sergei Meshveliani
mechvel at botik.ru
Mon Sep 17 15:12:01 CEST 2018
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
More information about the Agda
mailing list