diff options
author | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-20 13:13:49 +0000 |
---|---|---|
committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-20 13:13:49 +0000 |
commit | 55f59774cb3045374342c5b00f4a999b6ff0911b (patch) | |
tree | 8b76a59b1e4889db154d38c4e82d765751109b2a /test-suite/failure | |
parent | f078bd998a2e93857f6519f75bf456c6069086e5 (diff) |
Erreurs de Cases
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1650 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/failure')
-rw-r--r-- | test-suite/failure/Case1.v (renamed from test-suite/failure/case1.v) | 0 | ||||
-rw-r--r-- | test-suite/failure/Case10.v | 1 | ||||
-rw-r--r-- | test-suite/failure/Case11.v | 1 | ||||
-rw-r--r-- | test-suite/failure/Case12.v | 7 | ||||
-rw-r--r-- | test-suite/failure/Case13.v | 5 | ||||
-rw-r--r-- | test-suite/failure/Case14.v | 5 | ||||
-rw-r--r-- | test-suite/failure/Case2.v | 13 | ||||
-rw-r--r-- | test-suite/failure/Case3.v | 7 | ||||
-rw-r--r-- | test-suite/failure/Case4.v | 7 | ||||
-rw-r--r-- | test-suite/failure/Case5.v | 3 | ||||
-rw-r--r-- | test-suite/failure/Case6.v | 10 | ||||
-rw-r--r-- | test-suite/failure/Case7.v | 22 | ||||
-rw-r--r-- | test-suite/failure/Case8.v | 8 | ||||
-rw-r--r-- | test-suite/failure/Case9.v | 6 |
14 files changed, 95 insertions, 0 deletions
diff --git a/test-suite/failure/case1.v b/test-suite/failure/Case1.v index fafcafc1c..fafcafc1c 100644 --- a/test-suite/failure/case1.v +++ b/test-suite/failure/Case1.v diff --git a/test-suite/failure/Case10.v b/test-suite/failure/Case10.v new file mode 100644 index 000000000..ee47544df --- /dev/null +++ b/test-suite/failure/Case10.v @@ -0,0 +1 @@ +Type [x:nat]<nat> Cases x of ((S x) as b) => (S b) end. diff --git a/test-suite/failure/Case11.v b/test-suite/failure/Case11.v new file mode 100644 index 000000000..c39a76ca4 --- /dev/null +++ b/test-suite/failure/Case11.v @@ -0,0 +1 @@ +Type [x:nat]<nat> Cases x of ((S x) as b) => (S b x) end. diff --git a/test-suite/failure/Case12.v b/test-suite/failure/Case12.v new file mode 100644 index 000000000..b56eac0d9 --- /dev/null +++ b/test-suite/failure/Case12.v @@ -0,0 +1,7 @@ + +Type [x:nat]<nat> Cases x of + ((S x) as b) => <nat>Cases x of + x => x + end + end. + diff --git a/test-suite/failure/Case13.v b/test-suite/failure/Case13.v new file mode 100644 index 000000000..8a4d75b61 --- /dev/null +++ b/test-suite/failure/Case13.v @@ -0,0 +1,5 @@ +Type [x:nat]<nat> Cases x of + ((S x) as b) => <nat>Cases x of + x => (S b x) + end + end. diff --git a/test-suite/failure/Case14.v b/test-suite/failure/Case14.v new file mode 100644 index 000000000..887c038f6 --- /dev/null +++ b/test-suite/failure/Case14.v @@ -0,0 +1,5 @@ +Definition NIL := (Nil nat). +Type <(List nat)>Cases (Nil nat) of + NIL => NIL + | _ => NIL + end. diff --git a/test-suite/failure/Case2.v b/test-suite/failure/Case2.v new file mode 100644 index 000000000..183f612b0 --- /dev/null +++ b/test-suite/failure/Case2.v @@ -0,0 +1,13 @@ +Inductive IFExpr : Set := + Var : nat -> IFExpr + | Tr : IFExpr + | Fa : IFExpr + | IfE : IFExpr -> IFExpr -> IFExpr -> IFExpr. + +Type [F:IFExpr] + <Prop>Cases F of + (IfE (Var _) H I) => True + | (IfE _ _ _) => False + | _ => True + end. + diff --git a/test-suite/failure/Case3.v b/test-suite/failure/Case3.v new file mode 100644 index 000000000..2c651b877 --- /dev/null +++ b/test-suite/failure/Case3.v @@ -0,0 +1,7 @@ +Inductive List [A:Set] :Set := + Nil:(List A) | Cons:A->(List A)->(List A). + +Type [l:(List nat)]<nat>Cases l of + (Nil nat) =>O + | (Cons a l) => (S a) + end. diff --git a/test-suite/failure/Case4.v b/test-suite/failure/Case4.v new file mode 100644 index 000000000..d00c9a05f --- /dev/null +++ b/test-suite/failure/Case4.v @@ -0,0 +1,7 @@ + +Definition Berry := [x,y,z:bool] + Cases x y z of + true false _ => O + | false _ true => (S O) + | _ true false => (S (S O)) +end. diff --git a/test-suite/failure/Case5.v b/test-suite/failure/Case5.v new file mode 100644 index 000000000..bdb5544bb --- /dev/null +++ b/test-suite/failure/Case5.v @@ -0,0 +1,3 @@ +Inductive MS: Set := X:MS->MS | Y:MS->MS. + +Type [p:MS]<nat>Cases p of (X x) => O end. diff --git a/test-suite/failure/Case6.v b/test-suite/failure/Case6.v new file mode 100644 index 000000000..f588d275e --- /dev/null +++ b/test-suite/failure/Case6.v @@ -0,0 +1,10 @@ +Inductive List [A:Set] :Set := + Nil:(List A) | Cons:A->(List A)->(List A). + + +Type <(List nat)>Cases (Nil nat) of + NIL => NIL + | (CONS _ _) => NIL + + end. + diff --git a/test-suite/failure/Case7.v b/test-suite/failure/Case7.v new file mode 100644 index 000000000..3718f1989 --- /dev/null +++ b/test-suite/failure/Case7.v @@ -0,0 +1,22 @@ +Inductive listn : nat-> Set := + niln : (listn O) +| consn : (n:nat)nat->(listn n) -> (listn (S n)). + +Definition length1:= [n:nat] [l:(listn n)] + Cases l of + (consn n _ (consn m _ _)) => (S (S m)) + |(consn n _ _) => (S O) + | _ => O + end. + +Type [n:nat] + [l:(listn n)] + <nat>Cases n of + O => O + | (S n) => + <([_:nat]nat)>Cases l of + niln => (S O) + | l' => (length1 (S n) l') + end + end. + diff --git a/test-suite/failure/Case8.v b/test-suite/failure/Case8.v new file mode 100644 index 000000000..7f6bb6151 --- /dev/null +++ b/test-suite/failure/Case8.v @@ -0,0 +1,8 @@ +Inductive List [A:Set] :Set := + Nil:(List A) | Cons:A->(List A)->(List A). + +Type <nat>Cases (Nil nat) of + ((Nil_) as b) =>b + |((Cons _ _ _) as d) => d + end. + diff --git a/test-suite/failure/Case9.v b/test-suite/failure/Case9.v new file mode 100644 index 000000000..e8d8e89a3 --- /dev/null +++ b/test-suite/failure/Case9.v @@ -0,0 +1,6 @@ +Parameter compare : (n,m:nat)({(lt n m)}+{n=m})+{(gt n m)}. +Type <nat>Cases (compare O O) of + (* k<i *) (left _ _ (left _ _ _)) => O + | (* k=i *) (left _ _ _) => O + | (* k>i *) (right _ _ _) => O end. + |