The Coq mailing list

[AUGER C�dric <Cedric.Auger AT lri.fr>]

Satrajit Roy a écrit :
> Hi guys,
>  
> With reference to the following example, is there a way to forward
> reference Record y and use it in a function defined in Record x. For
> example, as an argument to createX or x''.
>  
> Thanks again.

I am not sure to understand your question, do you want a mutually
recursive definition of Record?
It is sadly not yet possible for inductive, and for co-inductive
(http://coq.inria.fr/V8.2beta/CHANGES),
I don't know, but (exepted for extraction purpouses) you can "emulate"
Records as they just are
syntactical sugar.

For example,
>
> CoInductive A : Set :=
> | cons : A -> B -> A
> with B : Set :=
> | cons2 : A -> B -> B
> .
> Notation "'{' 'A_field' '=' x ';' 'B_field' '=' y '}'" := (cons x y).
> Notation "'{' 'A_field2' '=' x ';' 'B_field2' '=' y '}'" := (cons2 x y).
>
> Definition A_field A := match A with cons x _ => x end.
> Definition B_field A := match A with cons _ x => x end.
> Definition A_field2 B := match B with cons2 x _ => x end.
> Definition B_field2 B := match B with cons2 _ x => x end.
> Notation "A '.(A_field)'" := (A_field A) (at level 100).
> Notation "A '.(B_field)'" := (B_field A) (at level 100).
> Notation "B '.(A_field2)'" := (A_field2 B) (at level 100).
> Notation "B '.(B_field2)'" := (B_field2 B) (at level 100).
stands for:
Record A : Set :=
cons {A_field : A; B_field : B}
with B : Set :=
 cons2 {A_field2 : A; B_field2 : B}.

(you even have better syntax as you can write {A_field = a; B_field = b}
instead of cons a b)

But send a more precise mail if I misunderstood you.

> ---------- Forwarded message ----------
> From: *Satrajit Roy* 
>Â <satrajit.roy AT gmail.com
>Â <mailto:satrajit.roy AT gmail.com>>
> Date: Tue, Nov 11, 2008 at 11:01 AM
> Subject: Re: Lists & Strings
> To: 
>Â coq-club AT pauillac.inria.fr
>  
>Â <mailto:coq-club AT pauillac.inria.fr>
>
>
> Hi guys,
>  
> How do I resolve the following:
>  
> Require Export List.
> Require Export String.
>  
> Module X.
>  
> Record x: Set := createX {
>   x': string;
>   x'' : bool
> }.
>  
> Record y: Set := createY {
>   y': string;
>   y'': list x;
>
>   y''': bool :=
>     match (length y') return bool with
>       | 0 => false
>       | _ => true
>   end;
>  
>   y'''' : bool  :=
>     match (length y'') return bool with
>       | 0 => false
>       | _ => true
>   end
> }.
>  
> End X.
>  
> which results in:
>  
> Error:
> In environment
> y' : string
> y'' : list x
> y''' := (match length y'' with
>          | 0 => false
>          | S _ => true
>          end:bool) : bool
> The term "y''" has type "list x" while it is expected to have type
> "string"
>  
> Thanks , as always, for your time and effort.
>