[Agda] --termination-depth

[Sergei Meshveliani]

People,
I have a function of the kind

  foo : MS -> ...
  foo (cons1 (cons2 ps _) _) =  ...

which is implemented by recursion by  ps : List Pair

contained under the two data constructors:  (cons1 (cons2 ps _) _).

And  Agda 2.4.2.2  reports of _failed termination_ for  foo.

I can fix this by copying  ps  to an additional argument used as a
counter for termination.

But before this, I tried   --termination-depth=4.
And this does not help.

1) Is this option for this case?
2) Where it is explained in the docs the "sized types" feature?

Thanks,

------
Sergei