[Agda] [ANNOUNCE] Agda 2.5.4.2

[Matthew Daggitt]

Hi Sergei,
 This is a change to the standard library. If you read the CHANGELOG for
v0.17 you will see that decidable equality has been moved to
`Data.Char.Unsafe`. It also explains the reasons for doing so.
Best,
Matthew

On Tue, Oct 30, 2018 at 1:01 PM Sergei Meshveliani <mechvel at botik.ru> wrote:

> On Mon, 2018-10-29 at 23:17 +0000, Andres Sicard Ramirez wrote:
> >  Dear all,
> >
> > The Agda Team is very pleased to announce the release of Agda 2.5.4.2.
> >
> > In this bug-fix release, we fixed a regression in Agda 2.5.4 related
> > to slow type-checking with unsolved instance constraint (this fix
> > wasn't included in the CHANGELOG by mistake, so see
> > https://github.com/agda/agda/issues/3177 ) and we fixed a regression
> > in Agda 2.5.4.1 related to the installation with some old versions of
> > `cabal-install`. See the details and other changes in
> >
> >     https://hackage.haskell.org/package/Agda-2.5.4.2/changelog
> >
> > [..]
>
>
> 1. What is, briefly, its relation to the Development version of
>    September 6, 2018 ?
>
> 2.
> Also I have a certain application tested under  Agda-2.5.3 + lib-0.16,
> and I try to port it to  Agda-2.5.4.2 + lib-0.17.
> This occurs difficult.
>
> For example, it imported _≟_ for Char by
>
>   open import Data.Char as Char using (Char) renaming (_≟_ to _≟c_)
>
> Now, I am somehow forced to write
>   open import Data.Char as Char using (Char)
>   ...
>   open StrictTotalOrder Char.strictTotalOrder using ()
>                                       renaming (_≟_ to _≟c_)
>
> Still this _≟c_ does not work as earlier. The code
>
>   delimiters =  ' ' ∷ ',' ∷ ';' ...
>
>   delimiter? :  Decidable (_∈ delimiters)
>   delimiter? c =  any (c ≟c_) delimiters
>
> is not type-checked any more. The report is
>
>   ℕ != Char of type Set
>   when checking that the expression any (c ≟c_) delimiters has type
>   Relation.Nullary.Dec (c ∈ delimiters)
>
> Has _≟_ changed its definition for Char ?
>
> Thanks,
>
> ------
> 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/20181030/6f865d15/attachment.html>