diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /test-suite/success/Case1.v |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'test-suite/success/Case1.v')
-rw-r--r-- | test-suite/success/Case1.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/success/Case1.v b/test-suite/success/Case1.v new file mode 100644 index 00000000..2d5a5134 --- /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) := + <P>Cases n of + O => H0 + | (S O) => H1 + | (S (S n)) => (H2 n (nat_ind2 n)) + end. +End NATIND2. + |