aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Case12.v
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-12-21 23:50:17 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-12-21 23:50:17 +0000
commit4d4f08acb5e5f56d38289e5629173bc1b8b5fd57 (patch)
treec160d442d54dbd15cbd0ab3500cdf94d0a6da74e /test-suite/success/Case12.v
parent960859c0c10e029f9768d0d70addeca8f6b6d784 (diff)
Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/Case12.v')
-rw-r--r--test-suite/success/Case12.v85
1 files changed, 42 insertions, 43 deletions
diff --git a/test-suite/success/Case12.v b/test-suite/success/Case12.v
index 284695f41..20073aa73 100644
--- a/test-suite/success/Case12.v
+++ b/test-suite/success/Case12.v
@@ -1,60 +1,59 @@
(* This example was proposed by Cuihtlauac ALVARADO *)
-Require PolyList.
+Require Import List.
-Fixpoint mult2 [n:nat] : nat :=
-Cases n of
-| O => O
-| (S n) => (S (S (mult2 n)))
-end.
+Fixpoint mult2 (n : nat) : nat :=
+ match n with
+ | O => 0
+ | S n => S (S (mult2 n))
+ end.
Inductive list : nat -> Set :=
-| nil : (list O)
-| cons : (n:nat)(list (mult2 n))->(list (S (S (mult2 n)))).
+ | nil : list 0
+ | cons : forall n : nat, list (mult2 n) -> list (S (S (mult2 n))).
Type
-[P:((n:nat)(list n)->Prop);
- f:(P O nil);
- f0:((n:nat; l:(list (mult2 n)))
- (P (mult2 n) l)->(P (S (S (mult2 n))) (cons n l)))]
- Fix F
- {F [n:nat; l:(list n)] : (P n l) :=
- <P>Cases l of
- nil => f
- | (cons n0 l0) => (f0 n0 l0 (F (mult2 n0) l0))
- end}.
+ (fun (P : forall n : nat, list n -> Prop) (f : P 0 nil)
+ (f0 : forall (n : nat) (l : list (mult2 n)),
+ P (mult2 n) l -> P (S (S (mult2 n))) (cons n l)) =>
+ fix F (n : nat) (l : list n) {struct l} : P n l :=
+ match l as x0 in (list x) return (P x x0) with
+ | nil => f
+ | cons n0 l0 => f0 n0 l0 (F (mult2 n0) l0)
+ end).
Inductive list' : nat -> Set :=
-| nil' : (list' O)
-| cons' : (n:nat)[m:=(mult2 n)](list' m)->(list' (S (S m))).
+ | nil' : list' 0
+ | cons' : forall n : nat, let m := mult2 n in list' m -> list' (S (S m)).
-Fixpoint length [n; l:(list' n)] : nat :=
- Cases l of
- nil' => O
- | (cons' _ m l0) => (S (length m l0))
+Fixpoint length n (l : list' n) {struct l} : nat :=
+ match l with
+ | nil' => 0
+ | cons' _ m l0 => S (length m l0)
end.
Type
-[P:((n:nat)(list' n)->Prop);
- f:(P O nil');
- f0:((n:nat)
- [m:=(mult2 n)](l:(list' m))(P m l)->(P (S (S m)) (cons' n l)))]
- Fix F
- {F [n:nat; l:(list' n)] : (P n l) :=
- <P>
- Cases l of
- nil' => f
- | (cons' n0 m l0) => (f0 n0 l0 (F m l0))
- end}.
+ (fun (P : forall n : nat, list' n -> Prop) (f : P 0 nil')
+ (f0 : forall n : nat,
+ let m := mult2 n in
+ forall l : list' m, P m l -> P (S (S m)) (cons' n l)) =>
+ fix F (n : nat) (l : list' n) {struct l} : P n l :=
+ match l as x0 in (list' x) return (P x x0) with
+ | nil' => f
+ | cons' n0 m l0 => f0 n0 l0 (F m l0)
+ end).
(* Check on-the-fly insertion of let-in patterns for compatibility *)
Inductive list'' : nat -> Set :=
-| nil'' : (list'' O)
-| cons'' : (n:nat)[m:=(mult2 n)](list'' m)->[p:=(S (S m))](list'' p).
-
-Check Fix length { length [n; l:(list'' n)] : nat :=
- Cases l of
- nil'' => O
- | (cons'' n l0) => (S (length (mult2 n) l0))
- end }.
+ | nil'' : list'' 0
+ | cons'' :
+ forall n : nat,
+ let m := mult2 n in list'' m -> let p := S (S m) in list'' p.
+
+Check
+ (fix length n (l : list'' n) {struct l} : nat :=
+ match l with
+ | nil'' => 0
+ | cons'' n l0 => S (length (mult2 n) l0)
+ end).