decidable_eq to decidable_pred

Stream: general

[Quanwen Chen]

If I have a type Q (Q : Type), and its equality is decidable, i.e., [decQ : decidable_eq Q], how can I say a function, λ q : Q, q = q is a decidable_pred?

[Eric Wieser]

Are you looking for λ q, deqQ q q?

[Quanwen Chen]

Thank you so much!

[Anne Baanen]

The typeclass system should be smart enough to figure this out as well, so you could write something like (by apply_instance : decidable_pred (@eq Q)).

[Eric Wieser]

That's not the instance being asked for here

[Eric Wieser]

That's defeq to deqQ in a reducible way

[Eric Wieser]

Admittedly needing decidability of x = x is a rather strange request, as it's just true!

[Quanwen Chen]

Thanks for all the help. I am trying to figure out how to use decidable_eq and decidable_pred within decidable type class, so I asked the trivial question.