The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

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.