[Agda] Termination Checking in Development Agda

[Nils Anders Danielsson]

On 2009-12-18 18:07, karim kanso wrote:
> Recently (about a week ago) I upgraded to the latest development
> version, I have noticed that a function that used to pass termination
> check now does not.

Your code is not accepted by Agda 2.2.0, 2.2.2 or 2.2.4.

> To the best of my understanding the function loop2path (below) uses
> guarded recursion so should pass the check.

The function loop2path is not guarded. One of the corecursive calls is
an argument to the function transfer, which is not a constructor.

--
/NAD