]> matita.cs.unibo.it Git - fireball-separation.git/blob - ocaml/lambda4.mli
bbfd13b990dd2f32b263f9e49a0b3bd2162ef3ac
[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