[Agda] strange termination check

[Nils Anders Danielsson]

On 2013-10-12 11:42, Sergei Meshveliani wrote:
> Is this difficult (if correct) to implement in Agda, say,
>                                    "termination by a proper subterm" ?

Agda does implement something like "termination by a proper subterm".
However, definitions of the following form are not supported (except
possibly via use of --termination-depth):

   f x = g (C x)  -- C x is not a subterm of x.

   g (C (D x)) = f x

Note also that if you use with or pattern-matching lambdas, then Agda
introduces auxiliary functions, and the termination-checker is applied
to the generated code, not (only) the code that you wrote.

-- 
/NAD