The Coq mailing list

[Martijn Vermaat <martijn AT vermaat.name>]

Op maandag 12-07-2010 om 16:30 uur [tijdzone -0700], schreef Taral:
> On Mon, Jul 12, 2010 at 4:07 PM, Paul Tarau 
> <paul.tarau AT gmail.com>
>  wrote:
> > In this case is it a good idea to define eqN by structural
> > induction or the built-in "=" relation should be used?
> 
> Use = whenever possible, in my experience. There's just so much stuff
> that can be used with = that can't be used with other relations
> without a lot of work.

I agree with that, but in this case it does not matter since it is
easily seen that eqN and = are the same relation on nat.

So I don't see a reason for using eqN, otherwise than giving you more
work.

cheers,
Martijn