The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 18/08/2016 11:31, Soegtrop, Michael wrote:
> my question was about the “have” in “has decidable equality”. What does
> make the decidable equality of a type available, so that Coq “has” it?
> There are lemmas like list_eq_dec in the standard library, but just
> having a lemma is not enough for Coq using it somehow automatically.

There has been a lot of confusion in this thread. While decidable
equality is the reason why it is possible in the first place, Coq does
not care about it at all. As Hugo explained, Coq just happens to
implement a limited version of the small inversion trick.

Best regards,

Guillaume