summaryrefslogtreecommitdiff
path: root/test-suite/success/Cases.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:23:14 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:23:14 +0200
commit86535d84cc3cffeee1dcd8545343f234e7285530 (patch)
tree9b221c283c2971f7ac151397231059e1d239e723 /test-suite/success/Cases.v
parent39efc41237ec906226a3a53d7396d51173495204 (diff)
parent61dc740ed1c3780cccaec00d059a28f0d31d0052 (diff)
Diffstat (limited to 'test-suite/success/Cases.v')
-rw-r--r--test-suite/success/Cases.v71
1 files changed, 46 insertions, 25 deletions
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 745529bf..f445ca8e 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -100,7 +100,7 @@ Type (fun x : nat => match x return nat with
| x => x
end).
-Section testlist.
+Module Type testlist.
Parameter A : Set.
Inductive list : Set :=
| nil : list
@@ -119,7 +119,6 @@ Definition titi (a : A) (l : list) :=
| nil => l
| cons b l => l
end.
-Reset list.
End testlist.
@@ -913,71 +912,77 @@ Type
| LeS n m _ => (S n, S m)
end).
-
+Module Type F_v1.
Fixpoint F (n m : nat) (h : Le n m) {struct h} : Le n (S m) :=
match h in (Le n m) return (Le n (S m)) with
| LeO m' => LeO (S m')
| LeS n' m' h' => LeS n' (S m') (F n' m' h')
end.
+End F_v1.
-Reset F.
-
+Module Type F_v2.
Fixpoint F (n m : nat) (h : Le n m) {struct h} : Le n (S m) :=
match h in (Le n m) return (Le n (S m)) with
| LeS n m h => LeS n (S m) (F n m h)
| LeO m => LeO (S m)
end.
+End F_v2.
(* Rend la longueur de la liste *)
-Definition length1 (n : nat) (l : listn n) :=
+
+Module Type L1.
+Definition length (n : nat) (l : listn n) :=
match l return nat with
| consn n _ (consn m _ _) => S (S m)
| consn n _ _ => 1
| _ => 0
end.
+End L1.
-Reset length1.
-Definition length1 (n : nat) (l : listn n) :=
+Module Type L1'.
+Definition length (n : nat) (l : listn n) :=
match l with
| consn n _ (consn m _ _) => S (S m)
| consn n _ _ => 1
| _ => 0
end.
+End L1'.
-
-Definition length2 (n : nat) (l : listn n) :=
+Module Type L2.
+Definition length (n : nat) (l : listn n) :=
match l return nat with
| consn n _ (consn m _ _) => S (S m)
| consn n _ _ => S n
| _ => 0
end.
+End L2.
-Reset length2.
-
-Definition length2 (n : nat) (l : listn n) :=
+Module Type L2'.
+Definition length (n : nat) (l : listn n) :=
match l with
| consn n _ (consn m _ _) => S (S m)
| consn n _ _ => S n
| _ => 0
end.
+End L2'.
-Definition length3 (n : nat) (l : listn n) :=
+Module Type L3.
+Definition length (n : nat) (l : listn n) :=
match l return nat with
| consn n _ (consn m _ l) => S n
| consn n _ _ => 1
| _ => 0
end.
+End L3.
-
-Reset length3.
-
-Definition length3 (n : nat) (l : listn n) :=
+Module Type L3'.
+Definition length (n : nat) (l : listn n) :=
match l with
| consn n _ (consn m _ l) => S n
| consn n _ _ => 1
| _ => 0
end.
-
+End L3'.
Type match LeO 0 return nat with
| LeS n m h => n + m
@@ -1256,7 +1261,7 @@ Type match (0, 0) with
| (x, y) => (S x, S y)
end.
-
+Module Type test_concat.
Parameter concat : forall A : Set, List A -> List A -> List A.
@@ -1273,6 +1278,7 @@ Type
| _, _ => Nil nat
end.
+End test_concat.
Inductive redexes : Set :=
| VAR : nat -> redexes
@@ -1295,7 +1301,6 @@ Type (fun n : nat => match n with
| _ => 0
end).
-Reset concat.
Parameter
concat :
forall n : nat, listn n -> forall m : nat, listn m -> listn (n + m).
@@ -1383,6 +1388,7 @@ Type
(* I.e. to test manipulation of elimination predicate *)
(* ===================================================================== *)
+Module Type test_term.
Parameter LTERM : nat -> Set.
Inductive TERM : Type :=
@@ -1397,7 +1403,8 @@ Type
| oper op1 l1, oper op2 l2 => False
| _, _ => False
end.
-Reset LTERM.
+
+End test_term.
@@ -1493,6 +1500,7 @@ Type
end.
+Module Type ff.
Parameter ff : forall n m : nat, n <> m -> S n <> S m.
Parameter discr_r : forall n : nat, 0 <> S n.
@@ -1505,6 +1513,7 @@ Type
| S x => or_intror (S x = 0) (discr_l x)
end).
+Module Type eqdec.
Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m :=
match n, m return (n = m \/ n <> m) with
@@ -1518,7 +1527,9 @@ Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m :=
end
end.
-Reset eqdec.
+End eqdec.
+
+Module Type eqdec'.
Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m :=
match n return (forall m : nat, n = m \/ n <> m) with
@@ -1540,6 +1551,7 @@ Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m :=
end
end.
+End eqdec'.
Inductive empty : forall n : nat, listn n -> Prop :=
intro_empty : empty 0 niln.
@@ -1554,7 +1566,10 @@ Type
| consn n a y as b => or_intror (empty (S n) b) (inv_empty n a y)
end).
-Reset ff.
+End ff.
+
+Module Type ff'.
+
Parameter ff : forall n m : nat, n <> m -> S n <> S m.
Parameter discr_r : forall n : nat, 0 <> S n.
Parameter discr_l : forall n : nat, S n <> 0.
@@ -1566,6 +1581,7 @@ Type
| S x => or_intror (S x = 0) (discr_l x)
end).
+Module Type eqdec.
Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m :=
match n, m return (n = m \/ n <> m) with
@@ -1578,7 +1594,10 @@ Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m :=
| or_intror h => or_intror (S x = S y) (ff x y h)
end
end.
-Reset eqdec.
+
+End eqdec.
+
+Module Type eqdec'.
Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m :=
match n return (forall m : nat, n = m \/ n <> m) with
@@ -1600,6 +1619,8 @@ Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m :=
end
end.
+End eqdec'.
+End ff'.
(* ================================================== *)
(* Pour tester parametres *)