[Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1

Sergei Meshveliani mechvel at botik.ru
Fri May 25 12:56:14 CEST 2018


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



More information about the Agda mailing list