Hi

I want to say "Let T be a type with decidable equality". How can I do it?

You can use Mathematical Components's eqType https://math-comp.github.io/htmldoc/mathcomp.ssreflect.eqtype.html.

with typeclasses, there is Stdpp's `Decision`

typeclass: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/base.v#L325

but some people just write out the sigma type, perhaps as a hypothesis or parameter

```
(T_eq_dec : forall (t t' : T), {t = t'}+{t <> t'})
```

(this is what `Decision`

uses under the hood)

Pavel Shuhray has marked this topic as resolved.

Last updated: Feb 01 2023 at 13:03 UTC