package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t = {
  1. ord : string ref;
  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. bool_select : string;
    (*

    name of the boolean selection function

    *)
  10. dot_file : string option;
    (*

    file to print the final state in

    *)
  11. dot_llproof : string option;
    (*

    file to print llproof

    *)
  12. dot_sat : bool;
    (*

    Print saturated set into DOT?

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

    prefix for printing checker proofs

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

    expand definitions

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

    initial interreduction of proof state?

    *)
  19. unary_depth : int;
    (*

    Maximum successive levels of unary inferences

    *)
  20. check : bool;
    (*

    check proof

    *)
}
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
val add_to_modes : string list -> (unit -> unit) -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct