diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-19 13:32:46 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-19 13:32:46 +0000 |
commit | d6868dcecd61bdc4a6e0c25097d22ce3cc7b8009 (patch) | |
tree | f8ac5c124b04870469fbd60434d72b8af62d939c /test-suite/success/Case8.v | |
parent | 1920bd1b98f649ba60ceb271207df93faa46dc2d (diff) |
Ces fichiers décrivent des comportements peut-être souhaités mais actuellement non implantés
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1996 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/Case8.v')
-rw-r--r-- | test-suite/success/Case8.v | 40 |
1 files changed, 0 insertions, 40 deletions
diff --git a/test-suite/success/Case8.v b/test-suite/success/Case8.v deleted file mode 100644 index 73b55028d..000000000 --- a/test-suite/success/Case8.v +++ /dev/null @@ -1,40 +0,0 @@ -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). - -Parameter inv_empty : (n,a:nat)(l:(listn n)) ~(empty (S n) (consn n a l)). - -Type -[n:nat] [l:(listn n)] - <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of - niln => (or_introl ? ~(empty O niln) intro_empty) - | ((consn n O y) as b) => (or_intror (empty (S n) b) ? (inv_empty n O y)) - | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y)) - - end. - - -Type -[n:nat] [l:(listn n)] - <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of - niln => (or_introl ? ~(empty O niln) intro_empty) - | (consn n O y) => (or_intror (empty (S n) (consn n O y)) ? - (inv_empty n O y)) - | (consn n a y) => (or_intror (empty (S n) (consn n a y)) ? - (inv_empty n a y)) - - end. - - - -Type -[n:nat] [l:(listn n)] - <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of - niln => (or_introl ? ~(empty O niln) intro_empty) - | ((consn O a y) as b) => (or_intror (empty (S O) b) ? (inv_empty O a y)) - | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y)) - - end. |