[Agda] Termination checking regression (Matrix-shaped orders?)

[Andrés Sicard-Ramírez]

On Thu, Mar 7, 2013 at 7:56 AM, Dominique Devriese
<dominique.devriese at cs.kuleuven.be> wrote:
> All,
>
> I have some code that used to termination check, but which no longer
> does with the Darcs version of Agda, perhaps due to the 18-2-2013
> change titled "Disabled matrix-shaped orders in the termination
> checker."?
>

Yes.

> The problem seems to be that (suc n, t) is no longer considered
> smaller than (n, lambda s t).

Right. Andreas explained how the pairs are compared after the above patch in

http://code.google.com/p/agda/issues/detail?id=787#c7

Maybe, it can help.

-- 
Andrés