[Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1

[Andrés Sicard-Ramírez]

On 23 May 2018 at 13:51, Sergei Meshveliani <mechvel at botik.ru> wrote:
>   > agda -c $agdaLibOpt GCDTest.agda
>
> MAlonzo/Code/Data/Colist.hs:295:11:
>     Couldn't match type ‘MAlonzo.RTE.Inf (T48 xa xA)’ with ‘[xA]’
>     Expected type: xA
>                    -> MAlonzo.RTE.Infinity xa (T48 xa xA) -> T48 xa xA
>       Actual type: xA -> [xA] -> [xA]
>     Relevant bindings include
>       check60 :: xA -> MAlonzo.RTE.Infinity xa (T48 xa xA) -> T48 xa xA
>         (bound at MAlonzo/Code/Data/Colist.hs:295:1)
>     In the expression: (:)
>     In an equation for ‘check60’: check60 = (:)

I have no problem using the *experimental* branch of the standard
library (but I could reproduce the above error using its *master*
branch).

Note that you should use the *experimental* branch of the standard
library with Agda 2.5.4 RC 1.


-- 
Andrés