Stream: Coq users

Topic: ✔ Decidable equality


view this post on Zulip Pavel Shuhray (Apr 05 2022 at 15:35):

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

view this post on Zulip Reynald Affeldt (Apr 05 2022 at 15:51):

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

view this post on Zulip Karl Palmskog (Apr 05 2022 at 16:11):

with typeclasses, there is Stdpp's Decision typeclass: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/base.v#L325

view this post on Zulip Karl Palmskog (Apr 05 2022 at 16:13):

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)

view this post on Zulip Notification Bot (Apr 23 2022 at 02:38):

Pavel Shuhray has marked this topic as resolved.


Last updated: Feb 01 2023 at 13:03 UTC