[Agda] missed termination failure

[mechvel at scico.botik.ru]

I have an impression that the attached M.agda has been deleted by some 
filter,
due to a problem with UTF symbols.
(?)

So I attach now  M.agda.zip.

--
SM


On 2019-10-28 16:29, mechvel at scico.botik.ru wrote:
> Dear Agda developers,
> 
> I wonder of whether the attached program presents a bug in the type
> checker of  2.6.0.1.
> The program is small.
> Its last line has
>               [y] = [y]          -- DEBUG
> instead of    [y] = [ y ]
> 
> The second version is type-checked fast.
> The first version probably needs a report like "Termination check 
> failed",
> but it hangs for a very long time.
> 
> Regards,
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
A non-text attachment was scrubbed...
Name: M.agda.zip
Type: application/zip
Size: 756 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191030/44621dc3/attachment.zip>