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: Taral <taralx AT gmail.com>
  • To: Paul Tarau <paul.tarau AT gmail.com>
  • Cc: julien forest <forest AT ensiie.fr>, coq-club AT inria.fr
  • Subject: Re: [Coq-Club] connecting the dots between Fixpoint definitions
  • Date: Mon, 12 Jul 2010 16:30:17 -0700
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; b=qbfS4hFT+EdMJsSHntamhfaaLrlq6wrS1ynpg5JgKQWzPrkzuA9qgOBtaogYsHC9OY gvtCTUdIxF/dzOjaqsVQ9j6N0JWDpyQzA4K2oMbpcqLLAgZGosfiLbpxzUYCc7a0wBew xQPsokg3RrQB1yYJ9eIpdv7CnfHD+tAleEfL0=
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.

Lemma cons_hd_tl : forall n, n = consN (hdN n) (tlN n).

-- 
Taral 
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
    -- Unknown


Archive powered by MhonArc 2.6.16.

Top of Page