The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

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?

V.