[Agda] agda error message

[Martin Escardo]

Thanks, Andreas. This is indeed the problem! The expression x does 
indeed have time X n, but for another n. One n (that of the type of x) 
is bound and the other is free! Martin

Andreas Abel wrote:
> 
> 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
> 
> 
>