[Agda] size-based termination

Ondrej Rypacek ondrej.rypacek at gmail.com
Tue Dec 21 16:30:55 CET 2010


Hi all,

I have a function which terminates for size but not structural reasons.

Is there a way to turn off the termination checker for this definition
so I can continue with the development ?

What is the best way of doing this properly ? I.e. how to turn a
size-terminating function into a structurally recursive one ?


Cheers,
Ondrej


More information about the Agda mailing list