summaryrefslogtreecommitdiff
path: root/test-suite/failure/inductive.v
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
commit7cfc4e5146be5666419451bdd516f1f3f264d24a (patch)
treee4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/failure/inductive.v
parent420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff)
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/failure/inductive.v')
-rw-r--r--test-suite/failure/inductive.v27
1 files changed, 27 insertions, 0 deletions
diff --git a/test-suite/failure/inductive.v b/test-suite/failure/inductive.v
new file mode 100644
index 00000000..f3e47bfd
--- /dev/null
+++ b/test-suite/failure/inductive.v
@@ -0,0 +1,27 @@
+(* A check that sort-polymorphic product is not set too low *)
+
+Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B.
+Fail Check (fun (A:Type) (B:Prop) => (prod A B : Prop)).
+Fail Check (fun (A:Prop) (B:Type) => (prod A B : Prop)).
+
+(* Check that the nested inductive types positivity check avoids recursively
+ non uniform parameters (at least if these parameters break positivity) *)
+
+Inductive t (A:Type) : Type := c : t (A -> A) -> t A.
+Fail Inductive u : Type := d : u | e : t u -> u.
+
+(* This used to succeed in versions 8.1 to 8.3 *)
+
+Require Import Logic.
+Require Hurkens.
+Definition Ti := Type.
+Inductive prod2 (X Y:Ti) := pair2 : X -> Y -> prod2 X Y.
+Fail Definition B : Prop := let F := prod2 True in F Prop. (* Aie! *)
+(*Definition p2b (P:Prop) : B := pair2 True Prop I P.
+Definition b2p (b:B) : Prop := match b with pair2 _ P => P end.
+Lemma L1 : forall A : Prop, b2p (p2b A) -> A.
+Proof (fun A x => x).
+Lemma L2 : forall A : Prop, A -> b2p (p2b A).
+Proof (fun A x => x).
+Check Hurkens.paradox B p2b b2p L1 L2.*)
+