The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

Inductive X: Type :=
Con {
    foo    : list nat;
    bar    : list X
    }.

will work.

I let someone else explain why it's not always the case, because I
don't really understand.

And also, I vote for a line or two about that in the documentation :-)

Alexandre


On Wed, Nov 30, 2011 at 2:09 PM, Nuno Gaspar 
<nmpgaspar AT gmail.com>
 wrote:
> X: Type :=
> Con {
>     foo    : list Stuff;
>     bar    : list X
>     }.