[Agda] strange termination check
Nils Anders Danielsson
nad at cse.gu.se
Tue Oct 15 07:48:38 CEST 2013
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.
More information about the Agda