Decomposition de Cases

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1651 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 15 insertions, 0 deletions

diff --git a/test-suite/success/Case6.v b/test-suite/success/Case6.v
new file mode 100644
index 000000000..1d5e3fb4e
--- /dev/null
+++ b/test-suite/success/Case6.v
@@ -0,0 +1,15 @@
+Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := 
+[m:nat]
+ <[n,m:nat] n=m \/ ~n=m>Cases n m of
+      O   O   => (or_introl ? ~O=O (refl_equal ? O))
+
+   |  O (S x) => (or_intror O=(S x) ? (discr_r x))
+
+   | (S x) O  => (or_intror ? ~(S x)=O (discr_l x))
+
+   | ((S x) as N) ((S y) as M) =>  
+      <N=M\/~N=M>Cases (eqdec x y) of
+        (or_introl h) => (or_introl  ? ~N=M (f_equal nat nat S x y h))
+      | (or_intror h) => (or_intror N=M ? (ff x y h))   
+      end
+ end.