The Coq mailing list

[Paolo Herms <paolo.herms AT inria.fr>]

Try this:

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

-- 
Paolo Herms
PhD Student - CEA Software Safety Lab. / INRIA ProVal Project
Paris, France


On Wednesday 30 November 2011 14:09:39 Nuno Gaspar wrote:
> Hello.
> 
> From what I saw, recursive records are not allowed in Coq. So one cannot do
> something like:
> 
> Record X: Type :=
> Con {
>     foo    : list Stuff;
>     bar    : list X
>     }.
> 
> Is there any way to go around this restriction? I mean what is the standard
> approach for a coq user to follow whenever faced with this situation?
> 
> Thank you!