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

Andrés Sicard-Ramírez andres.sicard.ramirez at gmail.com
Thu Mar 7 15:52:26 CET 2013

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."?


> 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


Maybe, it can help.


More information about the Agda mailing list