[Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1

[mechvel at scico.botik.ru]

On 2019-12-31 18:25, Guillaume Allais wrote:
> I'll add to that: if you perform all the recursive calls at the
> same time as `with comparePP e e'` then you should be able to get
> a terminating version of the function.
> 
> I am saying "should" because the example is not self-contained and
> as such it is impossible to test.
> 

A sigh of releaf!
The following is recognized as terminating:

------------------------------------------------
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)

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

So that we avoid a complication of introducing a counter.
This gives us a hope.
Without your "at the same time", it fails.




> On 31/12/2019 12: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.