From 6b8159d7522279211f2fd3d46fbcd8b6f8d3564e Mon Sep 17 00:00:00 2001 From: mohring Date: Fri, 20 Apr 2001 12:07:59 +0000 Subject: *** empty log message *** git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1648 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/success/Case1.v | 15 +++++++++++++++ test-suite/success/Case2.v | 11 +++++++++++ 2 files changed, 26 insertions(+) create mode 100644 test-suite/success/Case1.v create mode 100644 test-suite/success/Case2.v diff --git a/test-suite/success/Case1.v b/test-suite/success/Case1.v new file mode 100644 index 0000000000..2d5a51345b --- /dev/null +++ b/test-suite/success/Case1.v @@ -0,0 +1,15 @@ +(* Testing eta-expansion of elimination predicate *) + +Section NATIND2. +Variable P : nat -> Type. +Variable H0 : (P O). +Variable H1 : (P (S O)). +Variable H2 : (n:nat)(P n)->(P (S (S n))). +Fixpoint nat_ind2 [n:nat] : (P n) := +

Cases n of + O => H0 + | (S O) => H1 + | (S (S n)) => (H2 n (nat_ind2 n)) + end. +End NATIND2. + diff --git a/test-suite/success/Case2.v b/test-suite/success/Case2.v new file mode 100644 index 0000000000..0aa7b5beff --- /dev/null +++ b/test-suite/success/Case2.v @@ -0,0 +1,11 @@ +(* ============================================== *) +(* To test compilation of dependent case *) +(* Nested patterns *) +(* ============================================== *) + +Type <[n:nat]n=n>Cases O of + O => (refl_equal nat O) + | m => (refl_equal nat m) +end. + + -- cgit v1.2.3