<div dir="ltr"><div>> <span class="gmail-im"></span>
Most probably this issue is known, is indexed,<br>> probably other main developers would recall it.</div><div><br></div><div>I think the answer to this question could very well be "42": <a href="https://github.com/agda/agda/issues/42">https://github.com/agda/agda/issues/42</a></div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Aug 20, 2020 at 1:38 PM <<a href="mailto:mechvel@scico.botik.ru">mechvel@scico.botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On 2020-08-19 22:37, James Wood wrote:<br>
> Hi Sergei,<br>
> <br>
> This sounds like a fairly serious problem (the termination checker not<br>
> being run at the right time, or something). Do you have a minimal<br>
> working example?<br>
> <br>
<br>
Most probably this issue is known, is indexed,<br>
probably other main developers would recall it.<br>
If you write that it is difficult to find it, then I would probably try <br>
to reduce the example.<br>
<br>
Regards,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
<br>
> On 18/08/2020 19:00, <a href="mailto:mechvel@scico.botik.ru" target="_blank">mechvel@scico.botik.ru</a> wrote:<br>
>> Probably this has been discussed earlier, but for any occasion:<br>
>> I see that<br>
>>     begin ...<br>
>>           p ∙ (q ∙ (p' ∙ (b ∙ q'a)))<br>
>>     ∎<br>
>>     where  pp' = p ∙ p';  qq' = q ∙ q';  q'a = q'a<br>
>> <br>
>> is not type-checked in Agda 2.6.1 in a reasonable time.<br>
>> Needs it to report something like<br>
>> "Cycle in assignments: q'a = q'a "<br>
>> ?<br>
>> <br>
>> Regards,<br>
>> <br>
>> ------<br>
>> Sergei<br>
>> _______________________________________________<br>
>> Agda mailing list<br>
>> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
>> <br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>