[Agda] Ill shaped metavariable?

[Ondrej Rypacek]

Hi, thanks for your reply. But no, I'm importing only Data.Nat

Cheers,
Ondrej

On 15 November 2010 20:12, Larrytheliquid <larrytheliquid at gmail.com> wrote:
> 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:Dat
>>
>> 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
>
>