diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-20 20:31:42 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-20 20:31:42 +0000 |
commit | 63fe9ca9438693fcf4d601c05f77a4db50588b40 (patch) | |
tree | a5e2541e76ee6d32c67dcaaf9133480577e58857 /test-suite/failure/fixpoint4.v | |
parent | ea188f154f86960008df67fa0266a3aa648ff1e7 (diff) |
Added examples for checking that the guard condition excludes subterms
in impredicative types.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13024 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/failure/fixpoint4.v')
-rw-r--r-- | test-suite/failure/fixpoint4.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/failure/fixpoint4.v b/test-suite/failure/fixpoint4.v new file mode 100644 index 000000000..fd9563738 --- /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. |