[Agda] Termination checking regression (Matrix-shaped orders?)
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:
> 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
> 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