package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t = {
  1. ord : string;
  2. seed : int;
  3. steps : int;
  4. version : bool;
  5. timeout : float;
  6. prelude : (string, CCVector.ro) CCVector.t;
  7. files : (string, CCVector.ro) CCVector.t;
  8. select : string;
    (*

    name of the selection function

    *)
  9. dot_file : string option;
    (*

    file to print the final state in

    *)
  10. dot_llproof : string option;
    (*

    file to print llproof

    *)
  11. dot_sat : bool;
    (*

    Print saturated set into DOT?

    *)
  12. dot_all_roots : bool;
  13. dot_check : string option;
    (*

    prefix for printing checker proofs

    *)
  14. def_as_rewrite : bool;
  15. expand_def : bool;
    (*

    expand definitions

    *)
  16. stats : bool;
  17. presaturate : bool;
    (*

    initial interreduction of proof state?

    *)
  18. unary_depth : int;
    (*

    Maximum successive levels of unary inferences

    *)
  19. check : bool;
    (*

    check proof

    *)
  20. eta : [ `Reduce | `Expand | `None ];
    (*

    eta conversion

    *)
}
val parse_args : unit -> t
val default : t
val add_opt : (string * Arg.spec * string) -> unit
val add_opts : (string * Arg.spec * string) list -> unit
val add_to_mode : string -> (unit -> unit) -> unit