diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-20 17:00:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-20 17:00:38 +0000 |
| commit | 7d170e8e2ee9bc08bfb05f623190a51680410a37 (patch) | |
| tree | 9305d8e080a31dc34202bffa3981dbeedf4621f0 /test-suite/success/Inductive.v | |
| parent | d3f6e92fc69b5b64681cff285ab964b69cef5819 (diff) | |
Test bug 983
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7901 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/Inductive.v')
| -rw-r--r-- | test-suite/success/Inductive.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 33da5e4ce..1adcbd39a 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -42,3 +42,11 @@ Inductive Finite (A : Set) : LList A -> Prop := | Finite_LNil : Finite LNil | Finite_LCons : forall (a : A) (l : LList A), Finite l -> Finite (LCons a l). + +(* Check positivity modulo reduction (cf bug #983) *) + +Record P:Type := {PA:Set; PB:Set}. + +Definition F (p:P) := (PA p) -> (PB p). + +Inductive I_F:Set := c : (F (Build_P nat I_F)) -> I_F. |