[Agda] Termination problems with "with" and recursion

Jan Stolarek jan.stolarek at p.lodz.pl
Mon Dec 2 09:43:58 CET 2013


> My suggestion is to use --sized-types
Yes, I'm aware of that possibility, but it feels like a lot of boilerplate to get something other 
languages offer out-of-the-box. As a user I'd just like to see a better termination checker :-)

Janek


More information about the Agda mailing list