[Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1

[Sergei Meshveliani]

On Fri, 2018-05-25 at 13:04 +0200, Ulf Norell wrote:
> 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
> 

Thank you.
And I find that
           map (uncurry (\x y → (x , suc y))) ps

also works.

------
Sergei



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