diff options
| -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 33da5e4cee..1adcbd39a1 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. |