coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>
- To: Vladimir Voevodsky <vladimir AT ias.edu>
- Cc: Adam Chlipala <adamc AT hcoop.net>, Coq Club <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] an inductive types question
- Date: Sun, 11 Oct 2009 01:28:55 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On 11 Oct 2009, at 00:23, Vladimir Voevodsky wrote:
Excuse me, there was a typo. The correct text is:
Inductive I1 : Type := x0 : I1 | x1 : I1 | i : eq x0 x1 .
What I want here is a type such that for any type T, a function I1 - > T is given by a triple -- t1:T (its value on x0), t2:T (its value on x1) and e : eq t1 t2 .
Assuming that eq means equals, aren't two values which are the same not the same as one value?
T.
Also, the definition of Impl given below is meaningless.
V.
On Oct 10, 2009, at 5:42 PM, Adam Chlipala wrote:
Vladimir Voevodsky wrote:
Is there a way in Coq to make definitions such as:
Inductive I1 : Type := x0 : I1 | x1 : I1 | i : eq x0 x1 .
or
Inductive Impl : Type := P1: Prop | P2: Prop | impl: P1 -> P2 .
Neither of these fits the spirit of inductive definitions. In each example, you might want to assert the final "constructor" as an [Axiom] instead, but there is almost always a better way to do such things. We can't comment on the better way(s) for your specific situation without more background.
--------------------------------------------------------
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
--------------------------------------------------------
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
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
- [Coq-Club] Type hierarchy, (continued)
- [Coq-Club] Type hierarchy,
Jean-Francois Dufourd
- Re: [Coq-Club] Type hierarchy, André Hirschowitz
- Re: [Coq-Club] Type hierarchy, Hugo Herbelin
- Re: [Coq-Club] Type hierarchy, Adam Chlipala
- Re: [Coq-Club] Type hierarchy, Hugo Herbelin
- Re: [Coq-Club] Type hierarchy, Jean-Francois Dufourd
- [Coq-Club] Type hierarchy,
Jean-Francois Dufourd
- [Coq-Club] an inductive types question, Vladimir Voevodsky
- Re: [Coq-Club] an inductive types question, Adam Chlipala
- Re: [Coq-Club] an inductive types question, Vladimir Voevodsky
- Re: [Coq-Club] an inductive types question, Vladimir Voevodsky
- Re: [Coq-Club] an inductive types question, Thorsten Altenkirch
- Re: [Coq-Club] an inductive types question, Vladimir Voevodsky
- Re: [Coq-Club] an inductive types question, Adam Chlipala
- 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
- Re: [Coq-Club] an inductive types question, André Hirschowitz
- 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, Dan Doel
- [Coq-Club] another question (Prop as a subtype of Set), Vladimir Voevodsky
Archive powered by MhonArc 2.6.16.