[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