On 5 March 2015 at 10:28, Sergei Meshveliani <mechvel at botik.ru> wrote: > But before this, I tried --termination-depth=4. > And this does not help. > > 1) Is this option for this case? AFAIK, this option is obsolete (see https://github.com/agda/agda/commit/1ac6343c42b295649d6e66995fdf4e317d816630). -- Andrés