+type term =\r
+ | Var of int\r
+ | App of term * term\r
+ | Lam of term\r
+\r
exception ParsingError of string\r
\r
-val parse': string list -> Num.nf list * string list\r
-val problem_of_string:\r
+(* val problem_of_string:\r
string ->\r
string (* problem label *)\r
* Num.i_var option (* div *)\r
* Num.i_n_var list (* conv *)\r
* Num.i_n_var list (* ps *)\r
* string list (* names of free variables *)\r
+val from_file : string ->\r
+ (string (* problem label *)\r
+ * Num.i_var option (* div *)\r
+ * Num.i_n_var list (* conv *)\r
+ * Num.i_n_var list (* ps *)\r
+ * string list (* names of free variables *)) list *)\r
+\r
+ (* parses a string to a term *)\r
+ val parse: string -> term\r
+ (* parse many strings/terms, and returns the list of parsed terms + the list of free variables; variable 0 is not used *)\r
+ val parse_many: string list -> term list * string list\r