]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/problems/w
Improved parsing
[fireball-separation.git] / ocaml / problems / w
index d55e1b83dd9efe6b49811244731e37cce8d3eef5..c603cfb13cbfe0b421ea9a1d86c47083e32ad8b3 100644 (file)
@@ -70,6 +70,7 @@ N c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e
 \r
 $! new failing problem\r
 # it is backtracking, but it shouldn't\r
+# why? well, D occurs in some C's\r
 D (a b)\r
 C ((((((((a (v (y. y))) (v c)) ((x ((a (v (y. y))) (v c))) y)) (((a (v (y. y))) (((v c) ((((z z) b) (c. a)) (w (c. (v c))))) (w. (v. (z. (v (y. y))))))) (((v (x. (v c))) (v (x. (v c)))) (((((z z) b) (c. a)) (z z)) (b c))))) (a. ((((z z) b)(c. a)) (z z)))) (y. (z z))) (((a (v (y. y))) w) (z. x))) (w. (z. (v (y. y)))))\r
 C ((((((((z z) b) (c. a)) (z z)) ((v (y. y)) a)) (v (y. y))) ((((a (v (y. y))) (v c)) (z z)) ((a (v (y. y))) (((v c) ((((z z) b) (c. a)) (w (c. (v c))))) (w. (v. (z. (v (y. y))))))))) (z. ((v (y. y)) a)))\r