[Agda] --termination-depth

[Andreas Abel]

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.



-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/