[Agda] --termination-depth

[Sergei Meshveliani]

On Fri, 2015-03-06 at 13:23 +0100, Andreas Abel wrote:
> On 05.03.2015 21:01, Andrés Sicard-Ramírez wrote:
> > On 5 March 2015 at 12:56, Sergei Meshveliani <mechvel at botik.ru> wrote:
> >> If it is obsolete, then Agda probably needs to report this explicitly.
> >
> > I was wrong. The option is not obsolete.
> 
> No, it is not obsolete.  Due to performance penalty with unlimited 
> termination-depth, the default is still 1.  Here the relevant CHANGELOG:
> 
> 
> * The performance of the termination checker has been improved.  For
>    higher --termination-depth the improvement is significant.
>    While the default --termination-depth is still 1, checking with
>    higher --termination-depth should now be feasible.
> 

Anyway, must  "--termination-depth=4"  help in my example with the two
composed data constructors?

Where it is documented the "sized types" feature ?

Thanks,

------
Sergei