coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Why do we need modules anyway?

From: Chris Dams <chris.dams.nl AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Why do we need modules anyway?
Date: Sun, 17 Jan 2010 10:01:41 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type:content-transfer-encoding; b=H9fkAgfOmlZloBq8z0SGE9xH7Bqjv5cEXg2m9wIBV8x/7CfziOJ88OBpdHrwPn0qmF b2yEjyjc6Bqd+eE/yyCTdFLE81WEhbE2udHXd1QJaUC0s38nCv8VCMsnxMaMT1XYJI9F sEXv/rbVdBT30irnrSXq1HT7igHMSeeYGQi3g=

Dear Adam and St�phane and all the rest,

Thanks for the info. I see that modules may well be useful for some
people, but I think I will mostly be using records for things like my
list_type. I like records better in most cases, I think.

All the best,
Chris

[Coq-Club] Why do we need modules anyway?, Chris Dams
- Re: [Coq-Club] Why do we need modules anyway?, Adam Chlipala
  - Re: [Coq-Club] Why do we need modules anyway?, St�phane Lescuyer
    - Re: [Coq-Club] Why do we need modules anyway?, Chris Dams
    - Re: [Coq-Club] Why do we need modules anyway?, AUGER
      - Re: [Coq-Club] Why do we need modules anyway?, Roman Beslik
        
        Re: [Coq-Club] Why do we need modules anyway?, St�phane Lescuyer
      - Re: [Coq-Club] Why do we need modules anyway?, Bas Spitters
        
        [Coq-Club] Making universe inconsistency only using "Require", AUGER
        
        Re: [Coq-Club] Making universe inconsistency only using "Require", Vladimir Voevodsky
        
        Re: [Coq-Club] {|...|} Notation (was: Making universe inconsistency only using "Require"), AUGER
        
        Re: [Coq-Club] Making universe inconsistency only using "Require", roconnor