diff options
Diffstat (limited to 'test-suite/success/Case6.v')
-rw-r--r-- | test-suite/success/Case6.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/success/Case6.v b/test-suite/success/Case6.v new file mode 100644 index 00000000..a262251e --- /dev/null +++ b/test-suite/success/Case6.v @@ -0,0 +1,19 @@ +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 + 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. |