]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/problems.ml
Fixes to parser
[fireball-separation.git] / ocaml / problems.ml
index bd3e880092291adc104a140a3604e0a5917d0e6a..f2812775b2a3dc43dcf94e210ead6076e6b1c011 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 _ -> ()