The Coq mailing list

[Greg Morrisett <greg AT eecs.harvard.edu>]

Hi Nuno,

You could just use an inductive definition as in:
[[

Inductive X : Type := 
| Con : list Stuff -> list X -> X.

]]
Then you can define operations such as:
[[

Definition foo(x:X) : list Stuff := 
  match x with
  | Cons f b => f
  end.

Definition bar(x:X) : list X := 
  match x with 
  | Cons f b => b
  end.

]]

-Greg

On Nov 30, 2011, at 8:09 AM, 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.