[Agda] size-based termination

[Andreas Abel]

On 12/21/10 4:30 PM, Ondrej Rypacek wrote:
> 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 ?

{-# OPTIONS --no-termination-check #-}

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

Aeh.  Depends.  What about adding a dummy argument which is structurally 
decreasing in each recursive call?

With more concrete input I can give more concrete answers...

Cheers,
Andreas