coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vladimir Voevodsky <vladimir AT ias.edu>
- To: Coq Club <coq-club AT pauillac.inria.fr>
- Subject: [Coq-Club] another inductive types question
- Date: Sun, 11 Oct 2009 14:16:56 -0400
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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.
- [Coq-Club] another question (cont.), (continued)
- [Coq-Club] another question (cont.), Vladimir Voevodsky
- Re: [Coq-Club] another question (cont.), Taral
- [Coq-Club] About extraction and mutual recursion, AUGER Cédric
- [Coq-Club] Typo on coq manual, AUGER
- Re: [Coq-Club] Typo on coq manual, Pierre Letouzey
- Re: [Coq-Club] another question (Prop as a subtype of Set), Matthieu Sozeau
- Re: [Coq-Club] an inductive types question, Vladimir Voevodsky
- Re: [Coq-Club] an inductive types question, AUGER Cédric
- Re: [Coq-Club] an inductive types question, André Hirschowitz
- Re: [Coq-Club] an inductive types question, AUGER Cédric
- [Coq-Club] another inductive types question, Vladimir Voevodsky
- Re: [Coq-Club] another inductive types question, AUGER Cédric
- Re: [Coq-Club] another inductive types question, Roman Beslik
- Re: [Coq-Club] another inductive types question, Vladimir Voevodsky
- Re: [Coq-Club] Type hierarchy, Randy Pollack
Archive powered by MhonArc 2.6.16.