[Agda] type-checking x=x
mechvel at scico.botik.ru
mechvel at scico.botik.ru
Thu Aug 20 13:36:22 CEST 2020
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 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
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
More information about the Agda
mailing list