coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Roman Beslik <beroal AT ukr.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Why do we need modules anyway?
Date: Tue, 19 Jan 2010 10:38:29 +0200
Disposition-notification-to: Roman Beslik <beroal AT ukr.net>

Hello.
I thought that "Record" automatically creates projections (field labels), but "Inductive" does not. Is it true?
On 18.01.10 14:38, AUGER wrote:

Records (as they just are Inductives, and cannot be used inside mutual inductives for stupid reasons)

[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