Module Params

module Params: sig .. end

Parameters for the prover, etc.

type t = {

`param_ord : string;`
`param_seed : int;`
`param_steps : int;`
`param_version : bool;`
`param_timeout : float;`
`param_files : (string, CCVector.ro) CCVector.t;`
`param_select : string;`	`(*`	name of the selection function	`*)`
`param_dot_file : string option;`	`(*`	file to print the final state in	`*)`
`param_dot_sat : bool;`	`(*`	Print saturated set into DOT?	`*)`
`param_dot_all_roots : bool;`
`param_expand_def : bool;`	`(*`	expand definitions	`*)`
`param_stats : bool;`
`param_presaturate : bool;`	`(*`	initial interreduction of proof state?	`*)`
`param_unary_depth : int;`	`(*`	Maximum successive levels of unary inferences	`*)`

}

val ord : string Pervasives.ref

val seed : int Pervasives.ref

val steps : int Pervasives.ref

val version : bool Pervasives.ref

val timeout : float Pervasives.ref

val presaturate : bool Pervasives.ref

val dot_file : string option Pervasives.ref

val dot_sat : bool Pervasives.ref

val dot_all_roots : bool Pervasives.ref

val expand_def : bool Pervasives.ref

val select : string Pervasives.ref

val unary_depth : int Pervasives.ref

val files : (string, CCVector.rw) CCVector.t

val parse_args : unit -> t

parse_args returns parameters

val add_opt : string * Arg.spec * string -> unit

val add_opts : (string * Arg.spec * string) list -> unit

val key : t Flex_state.key