[Agda] Termination problems with "with" and recursion

Nils Anders Danielsson nad at cse.gu.se
Tue Nov 19 10:36:50 CET 2013

On 2013-11-18 11:49, Jan Stolarek wrote:
> I am now writing a merge function for trees and I've hit the same
> problem again.

Ulf recently changed Agda to reduce the need for workarounds:

   Issue 59: Improving termination checking of functions defined using

You may want to try the latest development version.


More information about the Agda mailing list