blob: 1e17d090c222dd5e7eb589d391ab84a87d233a82 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(* -*- mode: coq; coq-prog-args: ("-allow-sprop") -*- *)
Check SProp.
Definition iUnit : SProp := forall A : SProp, A -> A.
Definition itt : iUnit := fun A a => a.
Definition iSquash (A:Type) : SProp
:= forall P : SProp, (A -> P) -> P.
Definition isquash A : A -> iSquash A
:= fun a P f => f a.
Fail Check (fun A : SProp => A : Type).
Lemma foo : Prop.
Proof. pose (fun A : SProp => A : Type). Abort.
(* define evar as product *)
Check (fun (f:(_:SProp)) => f _).
|
