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

[Andrés Sicard-Ramírez]

On 19 June 2014 11:24, Brent Yorgey <byorgey at seas.upenn.edu> wrote:

> I just upgraded to Agda 2.4.0.1 and now compiling the library generates
> the error
>
>
Please note that Agda 2.4.0.1 is an unreleased version (but I know it
is in Hackage).


>    Termination checking failed for the following functions:
>     Decision-procedures.List.Dec._≟_
>   Problematic calls:
>     ((x ∷ xs) ≟ (y ∷ ys)) (x ≟A₁ y)
>       (at
> /home/brent/src/equality/Equality/Decision-procedures.agda:238,14-15)
>   when scope checking the declaration
>     import Equality.Decision-procedures as
> .#Equality.Decision-procedures-131098778
>

It is due to a change on the behaviour of the termination-checker when
using the --without-K option (by removing this option, the function is
accepted).

-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140619/73e52541/attachment.html