The Coq mailing list

[Jonas Oberhauser <s9joober AT googlemail.com>]

Maybe the tactic "decide equality" can help you.

Note that not all types are decidable on equality and sometimes you'd
like a different equivalence relation.

Kind regards, Jonas

2012/4/29 Bernard Hurley 
<bernard AT marcade.biz>:
> Hi Jonas,
>
> Thanks for replying so soon. I will have a look at the implementation of 
> eq_nat_dec as I'm interested doing something like this in other situations.
> I guess in general it would depend on the exact nature of the solution of 
> the word problem for the type, and that there is no general solution.
>
> Cheers,
> Bernard.
>
> On Sun, Apr 29, 2012 at 07:25:45PM +0200, Jonas Oberhauser wrote:
>> Definition g f m n := if eq_nat_dec n m then 2 else f n.
>>
>> Using Coq.Arith.Peano_dec
>>