[Agda] import Data.Maybe.Core X import Data.Maybe

[Nils Anders Danielsson]

On 2013-07-01 21:30, Carlos Camarao wrote:
> open import Data.Maybe.Core            using (just) -- line 1
> -- open import Data.Maybe                 using (just) -- error (commenting line 1)
> open import Relation.Binary.Core       using (refl; _≡_)

This is not really related to your problem, but I suggest that you don't
import Core modules directly. The standard library's README contains the
following text:

-- Some modules have names ending in ".Core". These modules are
-- internal, and have (mostly) been created to avoid mutual recursion
-- between modules. They should not be imported directly; their
-- contents are reexported by other modules.

-- 
/NAD