coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- RE: [Coq-Club] connecting the dots between Fixpoint definitions, (continued)
- RE: [Coq-Club] connecting the dots between Fixpoint definitions,
Georges Gonthier
- Re: [Coq-Club] connecting the dots between Fixpoint definitions,
Paul Tarau
- RE: [Coq-Club] connecting the dots between Fixpoint definitions,
Georges Gonthier
- RE: [Coq-Club] connecting the dots between Fixpoint definitions, Georges Gonthier
- RE: [Coq-Club] connecting the dots between Fixpoint definitions,
Georges Gonthier
- Re: [Coq-Club] connecting the dots between Fixpoint definitions,
Paul Tarau
- Re: [Coq-Club] connecting the dots between Fixpoint definitions,
julien forest
- Re: [Coq-Club] connecting the dots between Fixpoint definitions, Paul Tarau
- Re: [Coq-Club] connecting the dots between Fixpoint definitions,
Paul Tarau
- Re: [Coq-Club] connecting the dots between Fixpoint definitions,
julien forest
- Re: [Coq-Club] connecting the dots between Fixpoint definitions,
Paul Tarau
- Re: [Coq-Club] connecting the dots between Fixpoint definitions,
Taral
- Re: [Coq-Club] connecting the dots between Fixpoint definitions, Martijn Vermaat
- Re: [Coq-Club] connecting the dots between Fixpoint definitions, AUGER Cedric
- Re: [Coq-Club] connecting the dots between Fixpoint definitions,
Taral
- Re: [Coq-Club] connecting the dots between Fixpoint definitions,
Paul Tarau
- Re: [Coq-Club] connecting the dots between Fixpoint definitions,
julien forest
- RE: [Coq-Club] connecting the dots between Fixpoint definitions,
Georges Gonthier
Archive powered by MhonArc 2.6.16.