Skip to content

Commit 2325f5a

Browse files
NegabinaryNegabinary
committed
Delete the list axioms too
1 parent 2eb5381 commit 2325f5a

File tree

1 file changed

+119
-119
lines changed

1 file changed

+119
-119
lines changed

‎src/language/proof/Axioms.re‎

Lines changed: 119 additions & 119 deletions
Original file line numberDiff line numberDiff line change
@@ -17,123 +17,123 @@ let v: ProofCtx.t =
1717
|> Exp.fresh,
1818
)
1919
|> Exp.fresh,
20-
)
21-
|> ProofCtx.add_exp(
22-
"Identity(@)R",
23-
Forall(
24-
Asc(
25-
Var("xs") |> Pat.fresh,
26-
List(Unknown(Internal) |> Typ.temp) |> Typ.fresh,
27-
)
28-
|> Pat.fresh,
29-
BinOp(
30-
Poly(Equals),
31-
ListConcat(Var("xs") |> Exp.fresh, ListLit([]) |> Exp.fresh)
32-
|> Exp.fresh,
33-
Var("xs") |> Exp.fresh,
34-
)
35-
|> Exp.fresh,
36-
)
37-
|> Exp.fresh,
38-
)
39-
|> ProofCtx.add_exp(
40-
"Identity(@)L",
41-
Forall(
42-
Asc(
43-
Var("xs") |> Pat.fresh,
44-
List(Unknown(Internal) |> Typ.temp) |> Typ.fresh,
45-
)
46-
|> Pat.fresh,
47-
BinOp(
48-
Poly(Equals),
49-
ListConcat(ListLit([]) |> Exp.fresh, Var("xs") |> Exp.fresh)
50-
|> Exp.fresh,
51-
Var("xs") |> Exp.fresh,
52-
)
53-
|> Exp.fresh,
54-
)
55-
|> Exp.fresh,
56-
)
57-
|> ProofCtx.add_exp(
58-
"Assoc(::, @)",
59-
Forall(
60-
Asc(Var("x") |> Pat.fresh, Unknown(Internal) |> Typ.fresh)
61-
|> Pat.fresh,
62-
Forall(
63-
Asc(
64-
Var("xs") |> Pat.fresh,
65-
List(Unknown(Internal) |> Typ.temp) |> Typ.fresh,
66-
)
67-
|> Pat.fresh,
68-
Forall(
69-
Asc(
70-
Var("ys") |> Pat.fresh,
71-
List(Unknown(Internal) |> Typ.temp) |> Typ.fresh,
72-
)
73-
|> Pat.fresh,
74-
BinOp(
75-
Poly(Equals),
76-
ListConcat(
77-
Cons(Var("x") |> Exp.fresh, Var("xs") |> Exp.fresh)
78-
|> Exp.fresh,
79-
Var("ys") |> Exp.fresh,
80-
)
81-
|> Exp.fresh,
82-
Cons(
83-
Var("x") |> Exp.fresh,
84-
ListConcat(Var("xs") |> Exp.fresh, Var("ys") |> Exp.fresh)
85-
|> Exp.fresh,
86-
)
87-
|> Exp.fresh,
88-
)
89-
|> Exp.fresh,
90-
)
91-
|> Exp.fresh,
92-
)
93-
|> Exp.fresh,
94-
)
95-
|> Exp.fresh,
96-
)
97-
|> ProofCtx.add_exp(
98-
"Assoc(@)",
99-
Forall(
100-
Asc(
101-
Var("xs") |> Pat.fresh,
102-
List(Unknown(Internal) |> Typ.temp) |> Typ.fresh,
103-
)
104-
|> Pat.fresh,
105-
Forall(
106-
Asc(
107-
Var("ys") |> Pat.fresh,
108-
List(Unknown(Internal) |> Typ.temp) |> Typ.fresh,
109-
)
110-
|> Pat.fresh,
111-
Forall(
112-
Asc(
113-
Var("zs") |> Pat.fresh,
114-
List(Unknown(Internal) |> Typ.temp) |> Typ.fresh,
115-
)
116-
|> Pat.fresh,
117-
BinOp(
118-
Poly(Equals),
119-
ListConcat(
120-
Var("xs") |> Exp.fresh,
121-
ListConcat(Var("ys") |> Exp.fresh, Var("zs") |> Exp.fresh)
122-
|> Exp.fresh,
123-
)
124-
|> Exp.fresh,
125-
ListConcat(
126-
ListConcat(Var("xs") |> Exp.fresh, Var("ys") |> Exp.fresh)
127-
|> Exp.fresh,
128-
Var("zs") |> Exp.fresh,
129-
)
130-
|> Exp.fresh,
131-
)
132-
|> Exp.fresh,
133-
)
134-
|> Exp.fresh,
135-
)
136-
|> Exp.fresh,
137-
)
138-
|> Exp.fresh,
13920
);
21+
// |> ProofCtx.add_exp(
22+
// "Identity(@)R",
23+
// Forall(
24+
// Asc(
25+
// Var("xs") |> Pat.fresh,
26+
// List(Unknown(Internal) |> Typ.temp) |> Typ.fresh,
27+
// )
28+
// |> Pat.fresh,
29+
// BinOp(
30+
// Poly(Equals),
31+
// ListConcat(Var("xs") |> Exp.fresh, ListLit([]) |> Exp.fresh)
32+
// |> Exp.fresh,
33+
// Var("xs") |> Exp.fresh,
34+
// )
35+
// |> Exp.fresh,
36+
// )
37+
// |> Exp.fresh,
38+
// )
39+
// |> ProofCtx.add_exp(
40+
// "Identity(@)L",
41+
// Forall(
42+
// Asc(
43+
// Var("xs") |> Pat.fresh,
44+
// List(Unknown(Internal) |> Typ.temp) |> Typ.fresh,
45+
// )
46+
// |> Pat.fresh,
47+
// BinOp(
48+
// Poly(Equals),
49+
// ListConcat(ListLit([]) |> Exp.fresh, Var("xs") |> Exp.fresh)
50+
// |> Exp.fresh,
51+
// Var("xs") |> Exp.fresh,
52+
// )
53+
// |> Exp.fresh,
54+
// )
55+
// |> Exp.fresh,
56+
// )
57+
// |> ProofCtx.add_exp(
58+
// "Assoc(::, @)",
59+
// Forall(
60+
// Asc(Var("x") |> Pat.fresh, Unknown(Internal) |> Typ.fresh)
61+
// |> Pat.fresh,
62+
// Forall(
63+
// Asc(
64+
// Var("xs") |> Pat.fresh,
65+
// List(Unknown(Internal) |> Typ.temp) |> Typ.fresh,
66+
// )
67+
// |> Pat.fresh,
68+
// Forall(
69+
// Asc(
70+
// Var("ys") |> Pat.fresh,
71+
// List(Unknown(Internal) |> Typ.temp) |> Typ.fresh,
72+
// )
73+
// |> Pat.fresh,
74+
// BinOp(
75+
// Poly(Equals),
76+
// ListConcat(
77+
// Cons(Var("x") |> Exp.fresh, Var("xs") |> Exp.fresh)
78+
// |> Exp.fresh,
79+
// Var("ys") |> Exp.fresh,
80+
// )
81+
// |> Exp.fresh,
82+
// Cons(
83+
// Var("x") |> Exp.fresh,
84+
// ListConcat(Var("xs") |> Exp.fresh, Var("ys") |> Exp.fresh)
85+
// |> Exp.fresh,
86+
// )
87+
// |> Exp.fresh,
88+
// )
89+
// |> Exp.fresh,
90+
// )
91+
// |> Exp.fresh,
92+
// )
93+
// |> Exp.fresh,
94+
// )
95+
// |> Exp.fresh,
96+
// )
97+
// |> ProofCtx.add_exp(
98+
// "Assoc(@)",
99+
// Forall(
100+
// Asc(
101+
// Var("xs") |> Pat.fresh,
102+
// List(Unknown(Internal) |> Typ.temp) |> Typ.fresh,
103+
// )
104+
// |> Pat.fresh,
105+
// Forall(
106+
// Asc(
107+
// Var("ys") |> Pat.fresh,
108+
// List(Unknown(Internal) |> Typ.temp) |> Typ.fresh,
109+
// )
110+
// |> Pat.fresh,
111+
// Forall(
112+
// Asc(
113+
// Var("zs") |> Pat.fresh,
114+
// List(Unknown(Internal) |> Typ.temp) |> Typ.fresh,
115+
// )
116+
// |> Pat.fresh,
117+
// BinOp(
118+
// Poly(Equals),
119+
// ListConcat(
120+
// Var("xs") |> Exp.fresh,
121+
// ListConcat(Var("ys") |> Exp.fresh, Var("zs") |> Exp.fresh)
122+
// |> Exp.fresh,
123+
// )
124+
// |> Exp.fresh,
125+
// ListConcat(
126+
// ListConcat(Var("xs") |> Exp.fresh, Var("ys") |> Exp.fresh)
127+
// |> Exp.fresh,
128+
// Var("zs") |> Exp.fresh,
129+
// )
130+
// |> Exp.fresh,
131+
// )
132+
// |> Exp.fresh,
133+
// )
134+
// |> Exp.fresh,
135+
// )
136+
// |> Exp.fresh,
137+
// )
138+
// |> Exp.fresh,
139+
// );

0 commit comments

Comments
 (0)