]> matita.cs.unibo.it Git - fireball-separation.git/blob - ocaml/lambda4.mli
problems now contain a label and the names of the original free variables
[fireball-separation.git] / ocaml / lambda4.mli
1 type problem\r
2 \r
3 type response = [\r
4  | `CompleteSeparable of string\r
5  | `CompleteUnseparable of string\r
6  | `Uncomplete\r
7 ]\r
8 \r
9 type result = [\r
10  `Complete | `Uncomplete\r
11 ] * [\r
12  | `Separable of (int * Num.nf) list\r
13  | `Unseparable of string\r
14 ]\r
15 \r
16 val problem_of: div:(string option) -> conv:string list -> nums:string list -> problem * response\r
17 (* the following will soon replace the one above *)\r
18 val tmp: (string (* problem label *)\r
19 * Num.i_var option (* div *)\r
20 * Num.i_n_var list (* conv *)\r
21 * Num.i_n_var list (* ps *)\r
22 * string list (* names of free variables *)) -> problem * response\r
23 val solve: problem * response -> result\r