coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] an inductive types question

From: Vladimir Voevodsky <vladimir AT ias.edu>
To: Coq Club <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] an inductive types question
Date: Sat, 10 Oct 2009 17:32:28 -0400
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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 .

?

V.

Re: [Coq-Club] what are "levels" in Coq, (continued)