[Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1
mechvel at scico.botik.ru
mechvel at scico.botik.ru
Mon Dec 30 19:36:42 CET 2019
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
More information about the Agda
mailing list