The Coq mailing list

["Satrajit Roy" <satrajit.roy AT gmail.com>]

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.

---------- Forwarded message ----------
From: Satrajit Roy <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

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.