The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

> Why redefining of names from other files is allowed but from the  
> current file is not... I don't think it's important.

Yes, that's exactly what confused me. It would be very good if a  
command which causes a re-definition produced a warning.

V.



On Oct 11, 2009, at 3:25 PM, Roman Beslik wrote:

> 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.
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club