aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/fixpoint4.v
blob: bf6133f1c92d8331650620342cec6921d6d9459b (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
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))).

Fail 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.