From 4ac92a2aebe31ff4d5d2fce48701e5994391d7b9 Mon Sep 17 00:00:00 2001 From: xclerc Date: Fri, 20 Sep 2013 12:55:35 +0000 Subject: Merge "inductive?.v" tests into a single "inductive.v" test. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16798 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/failure/inductive.v | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 test-suite/failure/inductive.v (limited to 'test-suite/failure/inductive.v') diff --git a/test-suite/failure/inductive.v b/test-suite/failure/inductive.v new file mode 100644 index 000000000..143e8bb36 --- /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 prod (X Y:Ti) := pair : X -> Y -> prod X Y. +Fail Definition B : Prop := let F := prod True in F Prop. (* Aie! *) +(*Definition p2b (P:Prop) : B := pair True Prop I P. +Definition b2p (b:B) : Prop := match b with pair _ 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.*) + -- cgit v1.2.3