[Agda] Ill shaped metavariable?

[Larrytheliquid]

Make sure you're not importing an overloaded constructor. i.e. sometimes
even if the goal and variable signature look the same, one may be in fact be
using an overloaded constructor of a different type.

On Mon, Nov 15, 2010 at 9:42 AM, Ondrej Rypacek <ondrej.rypacek at gmail.com>wrote:

> Hi all,
> is this normal:
>
> Goal: _≡_ {IdObj G n} (⟦_⟧Obj {G} {n} x) (⟦_⟧Obj {G} {n} x')
> Have: _≡_ {IdObj G n} (⟦_⟧Obj {G} {n} x) (⟦_⟧Obj {G} {n} x')
>
> I.e. I have what is asked of me, but yet the goal wouldn't be accepted
> ? With an error which an error which doesn't make sense to me, and
> I've tripple-checked everything, so am really puzzled.
>
> The source is a bit complicated to be posted here, so I wanted to
> check whether this is possible at all (and if there are some likely
> causes) before trying to come up with a simpler example.
>
> Cheers,
> Ondrej
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>



-- 
Respectfully,
Larry Diehl
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20101115/6e7b076a/attachment.html