diff options
Diffstat (limited to 'test-suite/failure/Case7.v')
-rw-r--r-- | test-suite/failure/Case7.v | 22 |
1 files changed, 22 insertions, 0 deletions
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)] + <nat>Cases n of + O => O + | (S n) => + <([_:nat]nat)>Cases l of + niln => (S O) + | l' => (length1 (S n) l') + end + end. + |