<div dir="ltr">Hi Sergei,<div> 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.</div><div>Best,</div><div>Matthew</div></div><br><div class="gmail_quote"><div dir="ltr">On Tue, Oct 30, 2018 at 1:01 PM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On Mon, 2018-10-29 at 23:17 +0000, Andres Sicard Ramirez wrote:<br>
>  Dear all,<br>
> <br>
> The Agda Team is very pleased to announce the release of Agda 2.5.4.2.<br>
> <br>
> In this bug-fix release, we fixed a regression in Agda 2.5.4 related<br>
> to slow type-checking with unsolved instance constraint (this fix<br>
> wasn't included in the CHANGELOG by mistake, so see<br>
> <a href="https://github.com/agda/agda/issues/3177" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues/3177</a> ) and we fixed a regression<br>
> in Agda 2.5.4.1 related to the installation with some old versions of<br>
> `cabal-install`. See the details and other changes in<br>
> <br>
>     <a href="https://hackage.haskell.org/package/Agda-2.5.4.2/changelog" rel="noreferrer" target="_blank">https://hackage.haskell.org/package/Agda-2.5.4.2/changelog</a><br>
> <br>
> [..] <br>
<br>
<br>
1. What is, briefly, its relation to the Development version of  <br>
   September 6, 2018 ?<br>
<br>
2.<br>
Also I have a certain application tested under  Agda-2.5.3 + lib-0.16,<br>
and I try to port it to  Agda-2.5.4.2 + lib-0.17.<br>
This occurs difficult.<br>
<br>
For example, it imported _≟_ for Char by<br>
<br>
  open import Data.Char as Char using (Char) renaming (_≟_ to _≟c_)<br>
<br>
Now, I am somehow forced to write<br>
  open import Data.Char as Char using (Char) <br>
  ...<br>
  open StrictTotalOrder Char.strictTotalOrder using () <br>
                                      renaming (_≟_ to _≟c_)<br>
<br>
Still this _≟c_ does not work as earlier. The code<br>
<br>
  delimiters =  ' ' ∷ ',' ∷ ';' ...<br>
<br>
  delimiter? :  Decidable (_∈ delimiters)<br>
  delimiter? c =  any (c ≟c_) delimiters<br>
<br>
is not type-checked any more. The report is<br>
<br>
  ℕ != Char of type Set<br>
  when checking that the expression any (c ≟c_) delimiters has type<br>
  Relation.Nullary.Dec (c ∈ delimiters)<br>
<br>
Has _≟_ changed its definition for Char ?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>