[Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1

[mechvel at scico.botik.ru]

On 2019-12-31 15:23, Jesper Cockx wrote:
> From the changelog:
> 
>> The "with inlining" feature of the termination checker has been
>> removed. As a consequence, some functions defined using with are no
>> longer accepted as terminating. See Issue #59 for why this feature
>> was originally introduced and #3604 for why it had to be removed.
> 
> It is likely that your function no longer passes the termination
> checker because this feature was removed. There were several issues
> with the implementation of this feature and no-one was willing to
> maintain it, so unfortunately it had to be removed.
> 

Really, is it designed so that to fail to find termination for this:

-------------------------------------------------
open import Data.List using (List; []; _∷_)
open import Data.Nat using (ℕ; _<_)
open import Data.Nat.Properties using (_<?_)
open import Relation.Nullary using (Dec; yes; no)

f : List ℕ → List ℕ → List ℕ
f []       ys       =  ys
f xs       []       =  xs
f (x ∷ xs) (y ∷ ys) =  aux (x <? y)
   where
   aux : Dec (x < y) → List ℕ
   aux (yes _) =  y ∷ (f (x ∷ xs) ys)
   aux (no _)  =  x ∷ (f xs (y ∷ ys))
--------------------------------------------------
?

(I tried, and it reports "Termination checking failed").
If this is really so, then we sadly have to introduce a counter in many 
places.

--
SM