|
1 | 1 | let v: ProofCtx.t = |
2 | 2 | [] |
3 | | - |> ProofCtx.add_exp( |
4 | | - "Iden(+)L", |
5 | | - // Fun is being used as a stand-in for Forall |
6 | | - Forall( |
7 | | - Asc(Var("x") |> Pat.fresh, Atom(Int) |> Typ.fresh) |> Pat.fresh, |
8 | | - BinOp( |
9 | | - Poly(Equals), |
10 | | - BinOp( |
11 | | - Int(Plus), |
12 | | - Var("x") |> Exp.fresh, |
13 | | - Atom(Int(Bigint.zero)) |> Exp.fresh, |
14 | | - ) |
15 | | - |> Exp.fresh, |
16 | | - Var("x") |> Exp.fresh, |
17 | | - ) |
18 | | - |> Exp.fresh, |
19 | | - ) |
20 | | - |> Exp.fresh, |
21 | | - ) |
22 | | - |> ProofCtx.add_exp( |
23 | | - "Zero(*)", |
24 | | - Forall( |
25 | | - Asc(Var("x") |> Pat.fresh, Atom(Int) |> Typ.fresh) |> Pat.fresh, |
26 | | - BinOp( |
27 | | - Poly(Equals), |
28 | | - BinOp( |
29 | | - Int(Times), |
30 | | - Var("x") |> Exp.fresh, |
31 | | - Atom(Int(Bigint.zero)) |> Exp.fresh, |
32 | | - ) |
33 | | - |> Exp.fresh, |
34 | | - Atom(Int(Bigint.zero)) |> Exp.fresh, |
35 | | - ) |
36 | | - |> Exp.fresh, |
37 | | - ) |
38 | | - |> Exp.fresh, |
39 | | - ) |
40 | | - |> ProofCtx.add_exp( |
41 | | - "Comm(+)", |
42 | | - Forall( |
43 | | - Asc(Var("x") |> Pat.fresh, Atom(Int) |> Typ.fresh) |> Pat.fresh, |
44 | | - Forall( |
45 | | - Asc(Var("x") |> Pat.fresh, Atom(Int) |> Typ.fresh) |> Pat.fresh, |
46 | | - BinOp( |
47 | | - Poly(Equals), |
48 | | - BinOp(Int(Plus), Var("x") |> Exp.fresh, Var("y") |> Exp.fresh) |
49 | | - |> Exp.fresh, |
50 | | - BinOp(Int(Plus), Var("y") |> Exp.fresh, Var("x") |> Exp.fresh) |
51 | | - |> Exp.fresh, |
52 | | - ) |
53 | | - |> Exp.fresh, |
54 | | - ) |
55 | | - |> Exp.fresh, |
56 | | - ) |
57 | | - |> Exp.fresh, |
58 | | - ) |
59 | | - |> ProofCtx.add_exp( |
60 | | - "Assoc(+)", |
61 | | - Forall( |
62 | | - Asc(Var("x") |> Pat.fresh, Atom(Int) |> Typ.fresh) |> Pat.fresh, |
63 | | - Forall( |
64 | | - Asc(Var("x") |> Pat.fresh, Atom(Int) |> Typ.fresh) |> Pat.fresh, |
65 | | - Forall( |
66 | | - Asc(Var("x") |> Pat.fresh, Atom(Int) |> Typ.fresh) |> Pat.fresh, |
67 | | - BinOp( |
68 | | - Poly(Equals), |
69 | | - BinOp( |
70 | | - Int(Plus), |
71 | | - Var("x") |> Exp.fresh, |
72 | | - BinOp( |
73 | | - Int(Plus), |
74 | | - Var("y") |> Exp.fresh, |
75 | | - Var("z") |> Exp.fresh, |
76 | | - ) |
77 | | - |> Exp.fresh, |
78 | | - ) |
79 | | - |> Exp.fresh, |
80 | | - BinOp( |
81 | | - Int(Plus), |
82 | | - BinOp( |
83 | | - Int(Plus), |
84 | | - Var("x") |> Exp.fresh, |
85 | | - Var("y") |> Exp.fresh, |
86 | | - ) |
87 | | - |> Exp.fresh, |
88 | | - Var("z") |> Exp.fresh, |
89 | | - ) |
90 | | - |> Exp.fresh, |
91 | | - ) |
92 | | - |> Exp.fresh, |
93 | | - ) |
94 | | - |> Exp.fresh, |
95 | | - ) |
96 | | - |> Exp.fresh, |
97 | | - ) |
98 | | - |> Exp.fresh, |
99 | | - ) |
100 | | - |> ProofCtx.add_exp( |
101 | | - "Comm(*)", |
102 | | - Forall( |
103 | | - Asc(Var("x") |> Pat.fresh, Atom(Int) |> Typ.fresh) |> Pat.fresh, |
104 | | - Forall( |
105 | | - Asc(Var("x") |> Pat.fresh, Atom(Int) |> Typ.fresh) |> Pat.fresh, |
106 | | - BinOp( |
107 | | - Poly(Equals), |
108 | | - BinOp( |
109 | | - Int(Times), |
110 | | - Var("x") |> Exp.fresh, |
111 | | - Var("y") |> Exp.fresh, |
112 | | - ) |
113 | | - |> Exp.fresh, |
114 | | - BinOp( |
115 | | - Int(Times), |
116 | | - Var("y") |> Exp.fresh, |
117 | | - Var("x") |> Exp.fresh, |
118 | | - ) |
119 | | - |> Exp.fresh, |
120 | | - ) |
121 | | - |> Exp.fresh, |
122 | | - ) |
123 | | - |> Exp.fresh, |
124 | | - ) |
125 | | - |> Exp.fresh, |
126 | | - ) |
127 | | - |> ProofCtx.add_exp( |
128 | | - "Assoc(*)", |
129 | | - Forall( |
130 | | - Asc(Var("x") |> Pat.fresh, Atom(Int) |> Typ.fresh) |> Pat.fresh, |
131 | | - Forall( |
132 | | - Asc(Var("x") |> Pat.fresh, Atom(Int) |> Typ.fresh) |> Pat.fresh, |
133 | | - Forall( |
134 | | - Asc(Var("x") |> Pat.fresh, Atom(Int) |> Typ.fresh) |> Pat.fresh, |
135 | | - BinOp( |
136 | | - Poly(Equals), |
137 | | - BinOp( |
138 | | - Int(Times), |
139 | | - Var("x") |> Exp.fresh, |
140 | | - BinOp( |
141 | | - Int(Times), |
142 | | - Var("y") |> Exp.fresh, |
143 | | - Var("z") |> Exp.fresh, |
144 | | - ) |
145 | | - |> Exp.fresh, |
146 | | - ) |
147 | | - |> Exp.fresh, |
148 | | - BinOp( |
149 | | - Int(Times), |
150 | | - BinOp( |
151 | | - Int(Times), |
152 | | - Var("x") |> Exp.fresh, |
153 | | - Var("y") |> Exp.fresh, |
154 | | - ) |
155 | | - |> Exp.fresh, |
156 | | - Var("z") |> Exp.fresh, |
157 | | - ) |
158 | | - |> Exp.fresh, |
159 | | - ) |
160 | | - |> Exp.fresh, |
161 | | - ) |
162 | | - |> Exp.fresh, |
163 | | - ) |
164 | | - |> Exp.fresh, |
165 | | - ) |
166 | | - |> Exp.fresh, |
167 | | - ) |
168 | 3 | |> ProofCtx.add_exp( |
169 | 4 | "Reflexive(==)", |
170 | 5 | Forall( |
|
0 commit comments