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
|
import Library.WriteProof
import Library.ProofGraph
list = [-- create a var term, define a constant to it
"\"const\"","\"x\"","const","\"t1\"","typeOp","nil","opType","1","def","constTerm","0","def","defineConst",
-- hypothesis list for theorem
"nil",
-- equals name
"\"=\"","const",
-- equals type
"\"->\"","typeOp","1","ref","\"->\"","typeOp","1","ref","\"bool\"","typeOp","nil","opType","nil","cons","cons","opType",
"nil","cons","cons","opType",
-- equals term
"constTerm",
-- the constant
"\"const\"","const","1","remove","constTerm",
-- construct the equation of constant = variable
"appTerm",
"0","remove",
"appTerm",
"thm","pop"]
graph = doGraphGen list
fst3 :: (a,b,c) -> a
fst3 (a,_,_) = a
snd3 :: (a,b,c) -> b
snd3 (_,b,_) = b
thd3 :: (a,b,c) -> c
thd3 (_,_,c) = c
edgeCheck :: (Ord d) => (a,b,(c,d)) -> (e,f,(g,d)) -> Ordering
edgeCheck = (\a b -> compare (snd . thd3 $ a) (snd . thd3 $ b))
|
