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

Nils Anders Danielsson nad at chalmers.se
Thu Mar 7 18:15:38 CET 2013


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


More information about the Agda mailing list