coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: Lists & Strings

chronological Thread

From: "Satrajit Roy" <satrajit.roy AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Re: Lists & Strings
Date: Tue, 11 Nov 2008 11:01:46 -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=QHEJAmp26Nh5L/UNKZ1NO1GfS/DLgZYCDZklxNStJfGMUXawIrRCK1Lxx7kjS6aBQ3 dm/ZY14buOXbKW1tnQ/Ba4J3EFKHJjtVkI/luUBNQh2AwXpnTeeB/Jxa1lDtKNwuxBAu K4uvkXIFMB4ViPXWsZdhHMD85tQWNi5yWXnF0=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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.

[Coq-Club] Re: Lists & Strings, Satrajit Roy
- Re: [Coq-Club] Lists & Strings, Stéphane Glondu
  - Re: [Coq-Club] Lists & Strings, Satrajit Roy