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: Oct 13 2024 at 01:02 UTC