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

[Carlos Camarao]

Hi. Is the following ok, or a bug?

Compiling M.agda below with "import Data.Maybe.Core using (just)" is ok (no
error is detected), but
compiling with "import Data.Maybe using (just)" causes an error.

The error is: "Failed to infer the value of dotted pattern
                    when checking that the pattern .n has type A"

I am using agda version 2.3.0.1, on Ubuntu 12.04 LTS.

Carlos

=============
module M where

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; _≡_)

invJust : ∀ {A : Set} {n : A} {m : A} → (just n ≡ just m) → n ≡ m
invJust {A} {n} {.n} refl = refl

=============
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130701/a2286e54/attachment-0001.html