The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

On Tue, Jan 19, 2010 at 9:38 AM, Roman Beslik 
<beroal AT ukr.net>
 wrote:
> Hello.
> I thought that "Record" automatically creates projections (field labels),
> but "Inductive" does not. Is it true?

Yes it is, and there is special syntax for records as well. But I
think Cedric meant that they are just inductives in the sense that
these features are just helpers, they don't add anything to the
expressivity of the Coq language.

Stéphane
-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06