The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

Hi Emilio,

Have you got a small example of this technique that you could share?

Sincerely,

Saulo

On Mon, Feb 22, 2016 at 3:33 PM, Emilio Jesús Gallego Arias <e+coq-club AT x80.org> wrote:

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.