[Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1

[Ulf Norell]

This is a deliberate change to the type checker. See the second bullet point
in the changelog here:

https://github.com/agda/agda/blob/release-2.5.4/CHANGELOG.md#pattern-matching

and the corresponding issue

https://github.com/agda/agda/issues/2834

In your case the fix is to add a type signature to p (warning, untested
code):

  map (\ (p : _ × _) → let (x , y) = p in (x , suc y))  ps

/ Ulf

On Fri, May 25, 2018 at 12:56 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> On Sat, 2018-05-19 at 15:33 -0500, Andrés Sicard-Ramírez wrote:
> > Dear all,
> >
> > The Agda Team is very pleased to announce the first release candidate
> > of Agda 2.5.4. We plan to release 2.5.4 in one week.
> >
> > []
> >
> > Enjoy the RC and please test as much as possible.
> >
>
> On
>
> -------------------------------------------------
> open import Data.Product using (_×_; _,_)
> open import Data.List    using (List; map)
> open import Data.Nat     using (ℕ; suc)
>
> f : List (ℕ × ℕ) → List (ℕ × ℕ)
> f ps =
>      map (\p → let (x , y) = p in (x , suc y))  ps
> --------------------------------------------------
>
>
> Agda 2.5.3.20180519  reports
>
> /home/mechvel/agda/tosave/bugs/T.agda:7,21-26
> Cannot split on argument of non-datatype _A_10 ps
> when checking that the pattern x , y has type _A_10 ps
>
> Is this a bug in Agda?
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180525/84311431/attachment.html>