]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/problems.ml
Fixes to parser
[fireball-separation.git] / ocaml / problems.ml
index cd57451a70230816031c6264b75c7c16ab9f3dfe..cb4218c49068a8f29a0331c4bedcadbaf5f41f03 100644 (file)
@@ -1,6 +1,22 @@
 open Lambda4;;
 open Util;;
 
+(* Syntax for problem files in problem/ folder:
+
+- dollar ($) on newline
+  begin new problem
+  $! means that the problem is expected to be separable,
+  $? means that it is expected to be unseparable
+
+- (#) on new line
+  comment line
+
+- (D) (C) (N) stand respectively for divergent, convergent, numeric
+
+- lines starting with spaces inherit the type from the last line
+
+*)
+
 let assert_separable x =
  match solve x with
  | `Separable _ -> ()