[Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?

[Andrés Sicard-Ramírez]

On 20 June 2014 09:07, Brent Yorgey <byorgey at seas.upenn.edu> wrote:

> but is the code I linked now expected to
> fail termination checking?
>

Using the --without-K option? I don't know. This is an open issue and
people working on this issue know that the current behaviour is too
restrictive. I don't know if they are working in a better solution
right now.

-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140620/61fd97a9/attachment.html