Lines Matching refs:list
20 type solver = formula list -> thm list option stream
31 val solve : solver -> int -> formula list -> thm list list
32 val find : solver -> formula list -> thm list option
40 thms : thm list, (* Context, assumed consistent *)
41 hyps : thm list} (* Hypothesis, or set of support *)
62 val combine : (cost_fn * solver_node) list -> solver_node
78 type init_data = {limit : limit, thms : thm list, hyps : thm list}