coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: geng chen <chengeng4001 AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] A question about declaration and definition
- Date: Wed, 5 May 2010 14:06:02 +0800
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=AMEFRAsFdHZ80clujI22cjZwFl2X8AWPp6c946U0MKoOb/jWe0fu324uJJRrZS83cr 3fG0I0e+XJWW/Qyr08ZVGzk7PppIMzILV6MG0dO090YBgVCD/iq+h2oWNA1aZ3QGsmCq k1yQTaFNyp88ExOokJ8ExQd+gKCstObqu9K/k=
Hi everyone,
Recently, I need to develop a prototype in Coq. But I've met a problem, it seems naive, but it is important for me.
Inductive prim : Set :=
A : prim
| B : prim.
Inductive comp : Set := list all.
Inductive all : Set :=
C : prim -> all
| D : comp -> all.
Is there anyway to define the 3 types aboves? Do I need to use some special kinds of method to declare the type "all" in the front of the definition?
Thanks, best regards
Chen
- [Coq-Club] A question about declaration and definition, geng chen
Archive powered by MhonArc 2.6.16.