[Agda] Why is this non-terminating?

Jinwoo Lee jinwoo68 at gmail.com
Fri Jul 3 22:28:16 CEST 2020


Great. Thank you for the pointer, James.

On Fri, Jul 3, 2020 at 1:22 PM James Wood <james.wood.100 at strath.ac.uk> wrote:
>
> Okay, then probably this is the relevant issue:
> https://github.com/agda/agda/issues/59 .
> I know there have been a lot of changes to termination checking
> involving `with`, because it seems very hard to do it right.
>
> James


More information about the Agda mailing list