diff options
author | 2001-05-12 22:06:54 +0000 | |
---|---|---|
committer | 2001-05-12 22:06:54 +0000 | |
commit | d7ecf8102e94e691b37e30d755ddec92c6704efe (patch) | |
tree | 06448045f3b29e9ebc7bc3837681eeddfe06e17b | |
parent | 2a84370dce1e0f19cea46c473b1b2d236b72d9f8 (diff) |
Oubli d'hypotheses pour faire fonctionner les exemples
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1747 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | test-suite/success/Case3.v | 3 | ||||
-rw-r--r-- | test-suite/success/Case4.v | 4 | ||||
-rw-r--r-- | test-suite/success/Case6.v | 4 | ||||
-rw-r--r-- | test-suite/success/Case7.v | 3 |
4 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/success/Case3.v b/test-suite/success/Case3.v index 71429db49..e9dba1e3f 100644 --- a/test-suite/success/Case3.v +++ b/test-suite/success/Case3.v @@ -1,3 +1,6 @@ +Inductive Le : nat->nat->Set := + LeO: (n:nat)(Le O n) +| LeS: (n,m:nat)(Le n m) -> (Le (S n) (S m)). Parameter iguales : (n,m:nat)(h:(Le n m))Prop . diff --git a/test-suite/success/Case4.v b/test-suite/success/Case4.v index eaec5a52f..d8f14a4e1 100644 --- a/test-suite/success/Case4.v +++ b/test-suite/success/Case4.v @@ -1,3 +1,7 @@ +Inductive listn : nat-> Set := + niln : (listn O) +| consn : (n:nat)nat->(listn n) -> (listn (S n)). + Inductive empty : (n:nat)(listn n)-> Prop := intro_empty: (empty O niln). diff --git a/test-suite/success/Case6.v b/test-suite/success/Case6.v index 1d5e3fb4e..a262251e7 100644 --- a/test-suite/success/Case6.v +++ b/test-suite/success/Case6.v @@ -1,3 +1,7 @@ +Parameter ff: (n,m:nat)~n=m -> ~(S n)=(S m). +Parameter discr_r : (n:nat) ~(O=(S n)). +Parameter discr_l : (n:nat) ~((S n)=O). + Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := [m:nat] <[n,m:nat] n=m \/ ~n=m>Cases n m of diff --git a/test-suite/success/Case7.v b/test-suite/success/Case7.v index d0bb8ee63..6e2aea480 100644 --- a/test-suite/success/Case7.v +++ b/test-suite/success/Case7.v @@ -1,3 +1,6 @@ +Inductive List [A:Set] :Set := + Nil:(List A) | Cons:A->(List A)->(List A). + Inductive Empty [A:Set] : (List A)-> Prop := intro_Empty: (Empty A (Nil A)). |