Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] an inductive types question

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] an inductive types question


chronological Thread 
  • 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.





Archive powered by MhonArc 2.6.16.

Top of Page