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/failure/Case7.v | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 test-suite/failure/Case7.v (limited to 'test-suite/failure/Case7.v') diff --git a/test-suite/failure/Case7.v b/test-suite/failure/Case7.v new file mode 100644 index 00000000..3718f198 --- /dev/null +++ b/test-suite/failure/Case7.v @@ -0,0 +1,22 @@ +Inductive listn : nat-> Set := + niln : (listn O) +| consn : (n:nat)nat->(listn n) -> (listn (S n)). + +Definition length1:= [n:nat] [l:(listn n)] + Cases l of + (consn n _ (consn m _ _)) => (S (S m)) + |(consn n _ _) => (S O) + | _ => O + end. + +Type [n:nat] + [l:(listn n)] + Cases n of + O => O + | (S n) => + <([_:nat]nat)>Cases l of + niln => (S O) + | l' => (length1 (S n) l') + end + end. + -- cgit v1.2.3