<div dir="ltr"><div>From the changelog:<br><br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">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.<br></blockquote><br></div><div>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.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Dec 31, 2019 at 12:32 PM <<a href="mailto:mechvel@scico.botik.ru">mechvel@scico.botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">The below function _+ms_ satisfies the following property.<br>
<br>
For each pattern in the third clause for +ms there exists a nonempty <br>
subset js<br>
in the argument position set {1, 2} such that<br>
(for all i <- js,  argument(i)  is structurally greater than  <br>
argument(i)-on-RHS,<br>
  while the arguments at all other positions do not change <br>
syntactically).<br>
<br>
And by this rule, +ms is terminating.<br>
And a generalization of this rule is implemented in Agda.<br>
<br>
Am I missing something?<br>
<br>
If it is all right, then Agda-2.6.1 needs to follow Agda-2.6.0.1 at this <br>
point.<br>
<br>
?<br>
<br>
--<br>
SM<br>
<br>
<br>
On 2019-12-30 21:36, <a href="mailto:mechvel@scico.botik.ru" target="_blank">mechvel@scico.botik.ru</a> wrote:<br>
> On 2019-12-22 14:41, Andres Sicard Ramirez wrote:<br>
>> Dear all,<br>
>> <br>
>> The Agda Team is very pleased to announce the first release candidate<br>
>> of Agda 2.6.1. We plan to release 2.6.1 in three weeks.<br>
>> [..]<br>
> <br>
> This Agda-2.6.0.1.20191219 reports "Termination checking failed ..." <br>
> for<br>
> <br>
> --------------------------------<br>
> _+ms_ :  Op₂ (List Mon)<br>
> []                  +ms mons'                  =  mons'<br>
> mons                +ms []                     =  mons<br>
> ((monᶜ a e) ∷ mons) +ms ((monᶜ b e') ∷ mons')  with comparePP e e'<br>
> ...<br>
>     | tri> _ _ _ =  (monᶜ a e)  ∷ (mons +ms ((monᶜ b e') ∷ mons'))<br>
> ... | tri< _ _ _ =  (monᶜ b e') ∷ (((monᶜ a e) ∷ mons) +ms mons')<br>
> ... | tri≈ _ _ _ =  (monᶜ (a + b)  e) ∷ (mons +ms mons')<br>
> --------------------------------<br>
> <br>
> while Agda-2.6.0.1 type-checks this.<br>
> Which one is more correct?<br>
> <br>
> Among the arguments for +ms on RHS the first one is smaller by<br>
> construction than in LHS<br>
> (for tri>), or the second is smaller by construction than in LHS (for <br>
> tri<),<br>
> or each is smaller by construction than in LHS (for tri≈).<br>
> <br>
> --<br>
> SM<br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>