The Coq mailing list

[e+coq-club AT x80.org (Emilio Jesús Gallego Arias)]

Hi Saulo,

Saulo Araujo 
<saulo2 AT gmail.com>
 writes:

> Thanks a lot for your explanantion Artur. I have a feeling you are right
> and, sooner or later, I am gonna need the proof of the decidability of my
> dependent type. I am gonna keep it close to me :)

Note that if you can show an injection from your dependent type to a
type with decidable equality then you can transfer decidability (see
InjEqMixin in the math-comp library).

I find this trick quite useful when dealing with dependently-typed
syntax (as usually you can assume an upper bound), as usually my target
type is of the form { s : T | ... }.

Best,
E.