[Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1
mechvel at scico.botik.ru
mechvel at scico.botik.ru
Tue Dec 31 12:31:39 CET 2019
The below function _+ms_ satisfies the following property.
For each pattern in the third clause for +ms there exists a nonempty
subset js
in the argument position set {1, 2} such that
(for all i <- js, argument(i) is structurally greater than
argument(i)-on-RHS,
while the arguments at all other positions do not change
syntactically).
And by this rule, +ms is terminating.
And a generalization of this rule is implemented in Agda.
Am I missing something?
If it is all right, then Agda-2.6.1 needs to follow Agda-2.6.0.1 at this
point.
?
--
SM
On 2019-12-30 21:36, mechvel at scico.botik.ru wrote:
> On 2019-12-22 14:41, Andres Sicard Ramirez wrote:
>> Dear all,
>>
>> The Agda Team is very pleased to announce the first release candidate
>> of Agda 2.6.1. We plan to release 2.6.1 in three weeks.
>> [..]
>
> This Agda-2.6.0.1.20191219 reports "Termination checking failed ..."
> for
>
> --------------------------------
> _+ms_ : Op₂ (List Mon)
> [] +ms mons' = mons'
> mons +ms [] = mons
> ((monᶜ a e) ∷ mons) +ms ((monᶜ b e') ∷ mons') with comparePP e e'
> ...
> | tri> _ _ _ = (monᶜ a e) ∷ (mons +ms ((monᶜ b e') ∷ mons'))
> ... | tri< _ _ _ = (monᶜ b e') ∷ (((monᶜ a e) ∷ mons) +ms mons')
> ... | tri≈ _ _ _ = (monᶜ (a + b) e) ∷ (mons +ms mons')
> --------------------------------
>
> while Agda-2.6.0.1 type-checks this.
> Which one is more correct?
>
> Among the arguments for +ms on RHS the first one is smaller by
> construction than in LHS
> (for tri>), or the second is smaller by construction than in LHS (for
> tri<),
> or each is smaller by construction than in LHS (for tri≈).
>
> --
> SM
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
More information about the Agda
mailing list