The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Thank you both.
 

As I don't want to change definition, transparent decision procedure is nice and useful trick.

On Fri, Apr 22, 2016 at 6:54 PM, Daniel Schepler <dschepler AT gmail.com> wrote:

For the case of a decidable predicate, another workaround is to
rewrite it using a transparent decision procedure.  For example,
something like (untested):

Definition normalize_eq_nat {m n:nat} (e:m=n) : m=n :=
match eq_nat_dec m n with
| left e' => e'
| right ne => False_ind (ne e)
end.

(Apologies to whoever is due credit on this one, I forgot who it was
that posted this trick before.)
--
Daniel Schepler