From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- test-suite/success/Case1.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 test-suite/success/Case1.v (limited to 'test-suite/success/Case1.v') 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) := +

Cases n of + O => H0 + | (S O) => H1 + | (S (S n)) => (H2 n (nat_ind2 n)) + end. +End NATIND2. + -- cgit v1.2.3