aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/Uminus.v
blob: cc31c7ae6b87d84f47d8cfef9777c9a833a9a413 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
(* Check that the encoding of system U- fails *)

Require Hurkens.

Inductive prop : Prop := down : Prop -> prop.

(* Coq should reject the following access of a Prop buried inside
   a prop. *)

Fail Definition up (p:prop) : Prop := let (A) := p in A.

(* Otherwise, we would have a proof of False via Hurkens' paradox *)

Fail Definition paradox : False :=
 Hurkens.NoRetractFromSmallPropositionToProp.paradox
   prop
   down
   up
   (fun (A:Prop) (x:up (down A)) => (x:A))
   (fun (A:Prop) (x:A) => (x:up (down A)))
   False.