Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Fwd: Forward reference

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Fwd: Forward reference


chronological Thread 
  • From: "Satrajit Roy" <satrajit.roy AT gmail.com>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] Fwd: Forward reference
  • Date: Tue, 11 Nov 2008 12:12:52 -0500
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:mime-version:content-type; b=eqJHKs499lW4VQ4tRTXk2a9taIxSSEjKB+V9cIQpzozpKh45CmWKck736I4itRPTkR 3uDwToHV4Mi1pIcZortfIBmSk1BmtGV2KwFbHe4MiSon66BC4trf0ZNYVjSfut5Gcm8m MhBACKEYSZV90fneJKQgph51SMfu5xXcYFLdc=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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.




Archive powered by MhonArc 2.6.16.

Top of Page