[Agda] collections/containers/finite sets

[Daniel Schoepe]

On Mon, 14 Nov 2011 14:42:04 +0000, Ramana Kumar <rk436 at cam.ac.uk> wrote:
> Is it bad to use _≡_ for the equality? I tried to get Data.Char._==_,
> but it's not a relation and I didn't know how to turn it into one.

As far as I understand, it's fine to use _≡_ when talking about
relations. If you need to check for equality in a program (which is what
_==_ does), you can use _≟_ from Data.Char, which basically says that
_≡_ is decidable for Char.

Cheers,
Daniel
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 835 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20111115/5d7f1146/attachment.bin