[Agda] type-checking x=x

[James Wood]

Hi Sergei,

This sounds like a fairly serious problem (the termination checker not
being run at the right time, or something). Do you have a minimal
working example?

Regards,
James

On 18/08/2020 19:00, mechvel at scico.botik.ru wrote:
> Probably this has been discussed earlier, but for any occasion:
> I see that
>     begin ...
>           p ∙ (q ∙ (p' ∙ (b ∙ q'a)))
>     ∎
>     where  pp' = p ∙ p';  qq' = q ∙ q';  q'a = q'a
> 
> is not type-checked in Agda 2.6.1 in a reasonable time.
> Needs it to report something like
> "Cycle in assignments: q'a = q'a "
> ?
> 
> Regards,
> 
> ------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>