diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-06 09:20:30 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-06 09:20:30 +0000 |
commit | cbe658b0bdc3cdfcf768b0e8b84638c1df9bf8dc (patch) | |
tree | 8af3945da22fe73de148f9d0537aadcf3f9c8672 /test-suite/success/Inversion.v | |
parent | 6b3708ee25023860e533a3e4989a867e39574d0f (diff) |
Test de la correction d'un bug soumis par Dachuan Yu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3217 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/Inversion.v')
-rw-r--r-- | test-suite/success/Inversion.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v new file mode 100644 index 000000000..96ac86830 --- /dev/null +++ b/test-suite/success/Inversion.v @@ -0,0 +1,15 @@ +(* Submitted by Dachuan Yu (bug #220) *) +Fixpoint T[n:nat] : Type := + Cases n of + | O => (nat -> Prop) + | (S n') => (T n') + end. +Inductive R : (n:nat)(T n) -> nat -> Prop := + | RO : (Psi:(T O); l:nat) + (Psi l) -> (R O Psi l) + | RS : (n:nat; Psi:(T (S n)); l:nat) + (R n Psi l) -> (R (S n) Psi l). +Definition Psi00 : (nat -> Prop) := [n:nat] False. +Definition Psi0 : (T O) := Psi00. +Lemma Inversion_RO : (l:nat)(R O Psi0 l) -> (Psi00 l). +Inversion 1. |