The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

thank you for the very fast answers :-)

2011/11/30 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!

-- 
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.