[Agda] type-checking x=x

[Martin Escardo]

On 20/08/2020 12:50, Jesper at sikanda.be wrote:
>> Most probably this issue is known, is indexed,
>> probably other main developers would recall it.
> 
> I think the answer to this question could very well be "42":
> https://github.com/agda/agda/issues/42

I knew that the answer to the ultimate question of life, the universe,
and everything would be in github.

Martin


> 
> -- Jesper
> 
> On Thu, Aug 20, 2020 at 1:38 PM <mechvel at scico.botik.ru
> <mailto:mechvel at scico.botik.ru>> wrote:
> 
>     On 2020-08-19 22:37, James Wood wrote:
>     > 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?
>     >
> 
>     Most probably this issue is known, is indexed,
>     probably other main developers would recall it.
>     If you write that it is difficult to find it, then I would probably try
>     to reduce the example.
> 
>     Regards,
> 
>     ------
>     Sergei
> 
> 
> 
>     > On 18/08/2020 19:00, mechvel at scico.botik.ru
>     <mailto: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 <mailto:Agda at lists.chalmers.se>
>     >> https://lists.chalmers.se/mailman/listinfo/agda
>     >>
>     > _______________________________________________
>     > Agda mailing list
>     > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     > https://lists.chalmers.se/mailman/listinfo/agda
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe