-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathDemo.v
51 lines (34 loc) · 1011 Bytes
/
Demo.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
From CW Require Import Loader.
Axiom my_ax : True = False.
Lemma lemma1 : True = False.
Proof.
exact my_ax.
Qed.
Lemma lemma2 : True = False.
Admitted.
From Coq Require Classical.
Module Test.
Import Classical.
Lemma lemma3 : (2 = 3) \/ ~(2 = 3).
Proof.
apply classic.
Qed.
End Test.
CWGroup "Assumption Tests".
Fail CWAssert lemma1 Assumes.
CWAssert lemma1 Assumes my_ax.
Fail CWAssert lemma1 Assumes Classical_Prop.classic.
Fail CWAssert "lemma1" lemma1 Assumes lemma2.
CWAssert lemma1 Assumes Classical_Prop.classic my_ax.
Fail CWAssert "lemma2" lemma2 Assumes my_ax.
CWAssert Test.lemma3 Assumes Classical_Prop.classic my_ax.
Fail CWAssert Test.lemma3 Assumes my_ax.
CWEndGroup.
CWGroup "File Tests".
CWFile "theories/Demo.v" Size < 1100.
Fail CWFile "theories/Demo.v" Size < 200.
CWFile "theories/Demo.v" Matches "Axiom".
Fail CWFile "theories/Demo.v" Matches "$Theorem".
Fail CWFile "theories/Demo.v" Does Not Match "Axiom".
CWFile "theories/Demo.v" Does Not Match "$Theorem".
CWEndGroup.