Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] connecting the dots between Fixpoint definitions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] connecting the dots between Fixpoint definitions


chronological Thread 
  • From: Martijn Vermaat <martijn AT vermaat.name>
  • To: Taral <taralx AT gmail.com>
  • Cc: Paul Tarau <paul.tarau AT gmail.com>, coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] connecting the dots between Fixpoint definitions
  • Date: Tue, 13 Jul 2010 10:38:35 +0200

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





Archive powered by MhonArc 2.6.16.

Top of Page