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

[Dominique Devriese]

Great, I wasn't expecting it to be this easy, thanks!

Dominique

2013/3/7 Nils Anders Danielsson <nad at chalmers.se>:
> On 2013-03-07 13:56, Dominique Devriese wrote:
>>
>> Can anyone suggest an alternative way to make this termination check
>> with the current Agda?
>
>
> rec-builder P f = uncurry helper
>   where
>   helper...
>
> --
> /NAD
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda