[Agda] agda error message

[Andreas Abel]

On Jan 5, 2010, at 4:35 PM, Martin Escardo wrote:
> I get the following message:
>
>   n != n of type ℕ
>   when checking that the expression x has type X n
>
> I could try to show you the code, but maybe you have seen something  
> like this and know what it means.

Well, these are in fact different identifiers which are unfortunately  
printed both as "n".
[Such an error message has all the potential to drive me nuts. ;-)]

Without seeing the code I cannot say more about your problem.

Cheers,
Andreas

> A previous declaration does declare x to have type X n, and if I  
> postulate the offending definition, no error is reported (in  
> particular, the previously occurring x is accepted to have type X n).
>
> A bit of background: before I got a message that f (g n) != n.
> Then I proved that f (g n) = n, and applied the proof to the  
> corresponding code, using the following to get from X(f (g n)) to  
> the required X n.
>
> coersion : {I : Set} {X : I → Set} → {i j : I} → i ≡ j → X  
> i → X j
> coersion refl x = x
>
> But now agda is not happy with the complain n != n instead.
>
> Any ideas? The code is too big to send in a discussion message, but  
> I could try to isolate the error. I have used "coersion"  
> successfully in another part of the code to achieve the same effect.
>
> Thanks.
> Martin
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

Andreas ABEL
INRIA, Projet Pi.R2
23, avenue d'Italie
F-75013 Paris
Tel: +33.1.39.63.59.41