[Agda] strange termination check

[Sergei Meshveliani]

On Sat, 2013-10-12 at 13:42 +0400, Sergei Meshveliani wrote:
> On Sat, 2013-10-12 at 14:33 +0900, Andreas Abel wrote:
> > Unfortunately, the termination-depth-trick works only for natural 
> > numbers and sizes, not for lists and other data structures with a 
> > constructor that has more than one argument.
> > 
> 
> The consequence is that one does not know how to provide termination
> without complications brought with inductive types.
> For example, I tried to replace in the below example the step   
>        (b ∷ b' ∷ bs)  -->   b' ∷ bs
> 
> with one-level step, by denoting  b'' = b' :: bs  ...
> And failed.
> 
> Is this difficult (if correct) to implement in Agda, say, 
>                                   "termination by a proper subterm" ?

But if it is by the checker, then this is a hidden termination proof.
And when it is by an inductive type, it is (probably) a proof given as
an Agda data
(it this so?).
May be it has sense to provide an option like                      
                                  --use-termination-proof-by-subterm

Regards,

------
Sergei