coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
y''': bool :=
match (length y') return bool with
| 0 => false
| _ => true
end;
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.
Require Export String.
Module X.
Record x: Set := createX {
x': string;
x'' : bool
}.
x': string;
x'' : bool
}.
Record y: Set := createY {
y': string;
y'': list x;
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
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"
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.
- [Coq-Club] Fwd: Forward reference, Satrajit Roy
- Re: [Coq-Club] Fwd: Forward reference,
AUGER Cédric
- Re: [Coq-Club] Fwd: Forward reference,
Satrajit Roy
- Re: [Coq-Club] Fwd: Forward reference, AUGER Cédric
- Re: [Coq-Club] Fwd: Forward reference,
Satrajit Roy
- Re: [Coq-Club] Fwd: Forward reference,
AUGER Cédric
Archive powered by MhonArc 2.6.16.