The Coq mailing list

[Damien Pous <Damien.Pous AT ens-lyon.fr>]

Hi,

Since these definitions are not mutually dependent, the simplest thing
to do would be:

Inductive prim : Set :=
  A : prim
| B : prim.

Inductive all : Set :=
  C : prim -> all
| D : list all -> all.

Definition comp : Set := list all.


Otherwise, you can use the keyword "with" to define mutually recursive
inductives:

Inductive all : Set :=
  C : prim -> all
| D : comp -> all
with comp : Set :=
  nil: comp
| cons: all -> comp -> comp.


(in both cases, "Lemma ... with" might be useful to reason about the
corresponding types)

Best,
Damien


2010/5/5 geng chen 
<chengeng4001 AT gmail.com>:
>  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
>
>