[Agda] equality on Char

[James Wood]

Hi Sergei,

These are now just safe [0], and can be found in Data.Char and Data.String.

Regards,

James

[0]: https://github.com/agda/agda-stdlib/pull/640

On 24/01/2020 10:02, mechvel at scico.botik.ru wrote:
> Dear standard library developers,
> 
> In my certain old program it is written
> 
>   open import Data.Char.Unsafe using () renaming (_≟_ to _≟c_)
>   open import Data.String.Unsafe using (_≟_)
> 
> I recall that probably ".Unsafe" was appended in order to guarantee the
> equality to be solved
> fast on Char and String.
> But lib-1.2 does not find this modules.
> How is this feature treated in lib-1.2 ?
> 
> Thanks,
> 
> ------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda