coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vincent BENAYOUN <benayoun.vincent AT gmail.com>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] nat and Datatypes.nat
- Date: Fri, 28 Aug 2009 13:49:07 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=qJXeCs6sn9kHlh6MOnAaLonFF1saDzwDWrxcJR5BfUZj4nyviSEDZqAFRBxi4MZeeH 0sPa4QZZmBDalC+IHA/e5N+kfbpb/OxbIOirGTJQHqbm8Qrf5Acj4c0upR1GjCa/IKg5 D2PWx1u3u1lGSuxFw5q4lvs9W7TfiqZGZVhKY=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi,
Does anyone can explain me the signification of the error I get with the below example ?
Thank you in advance,
Vincent
Error message : The term "v" has type "nat" while it is expected to have type
"Datatypes.nat".
Require Import Coq.Strings.String.
Inductive my_records : Type :=
| My_EmptyRecord : my_records
| My_Record : forall A B:Type, string -> A -> my_records -> my_records.
Inductive my_restricted_records : Set :=
| Record1 : nat -> my_restricted_records
| Record2 : string -> nat -> my_restricted_records
| Record_other : my_restricted_records.
Definition records_convert (r : my_records) :=
match r with
| My_Record nat _ "a" v My_EmptyRecord => Record1 v
| My_Record string _ "b" b (My_Record nat _ "c" c My_EmptyRecord) => Record2 b c
| _ => Match0_other (* I need to be exhaustive *)
end.
Inductive my_records : Type :=
| My_EmptyRecord : my_records
| My_Record : forall A B:Type, string -> A -> my_records -> my_records.
Inductive my_restricted_records : Set :=
| Record1 : nat -> my_restricted_records
| Record2 : string -> nat -> my_restricted_records
| Record_other : my_restricted_records.
Definition records_convert (r : my_records) :=
match r with
| My_Record nat _ "a" v My_EmptyRecord => Record1 v
| My_Record string _ "b" b (My_Record nat _ "c" c My_EmptyRecord) => Record2 b c
| _ => Match0_other (* I need to be exhaustive *)
end.
- [Coq-Club] nat and Datatypes.nat, Vincent BENAYOUN
- Re: [Coq-Club] nat and Datatypes.nat, Adam Chlipala
Archive powered by MhonArc 2.6.16.