The Coq mailing list

[Roman Beslik <beroal AT ukr.net>]

Hello, Vladimir.
It's easy to grasp the meaning of the error if you clearly understand 
the syntax of "Inductive". Consider
 Inductive ST1:Type := nat : ST1 .
This declaration binds the name "ST1" to a newly generated inductive 
data type. Also it binds "nat" to the only *data constructor* of "ST1". 
(By the way, this "nat" has zero arguments.)

But "nat" was defined in the "Coq.Init.Datatypes" ("Coq.Init" files are 
included silently) earlier, you've *redefined* a quite standard name. So 
I guess that using "nat" here is a mistake. I see a similar problem in 
the second line
 Inductive ST2:Type  := ST1:ST2 .
where you bind "ST1" which is *already bound* in the first line. Why 
redefining of names from other files is allowed but from the current 
file is not... I don't think it's important.

Vladimir Voevodsky wrote:
> I am just trying to understand how the "Inductive" works. I also tried 
> the following:
> Inductive ST1:Type := nat : ST1 .
> Inductive ST2:Type  := ST1:ST2 .
> and the first line compiles while both lines together do not, with the 
> message  "Error: ST1 already exists".
> Is it right?
--

Best regards,
 Roman Beslik.