From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- test-suite/failure/fixpoint4.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 test-suite/failure/fixpoint4.v (limited to 'test-suite/failure/fixpoint4.v') diff --git a/test-suite/failure/fixpoint4.v b/test-suite/failure/fixpoint4.v new file mode 100644 index 00000000..fd956373 --- /dev/null +++ b/test-suite/failure/fixpoint4.v @@ -0,0 +1,19 @@ +(* Check that arguments of impredicative types are not considered + subterms even through commutative cuts on functional arguments + (example prepared by Bruno) *) + +Inductive IMP : Prop := + CIMP : (forall A:Prop, A->A) -> IMP +| LIMP : (nat->IMP)->IMP. + +Definition i0 := (LIMP (fun _ => CIMP (fun _ x => x))). + +Definition Paradox : False := + (fix F y o {struct o} : False := + match y with + | tt => fun f => + match f 0 with + | CIMP h => F y (h _ o) + | _ => F y (f 0) + end + end match o with LIMP f => f | _ => fun _ => o end) tt i0. -- cgit v1.2.3