package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val get_session_dir : allow_mkdir:bool -> string Queue.t -> string
val set_session_timelimit : int -> unit
val set_session_memlimit : int -> unit
exception Undefined_id of string
exception Number_of_arguments
type query =
  1. | Qnotask of Controller_itp.controller -> string list -> string
  2. | Qtask of Controller_itp.controller -> Trans.naming_table -> string list -> string
val print_id : 'a -> Trans.naming_table -> string list -> string
val search_id : search_both:bool -> 'a -> Trans.naming_table -> string list -> string
val list_strategies : Controller_itp.controller -> (string * string) list
val list_provers : Controller_itp.controller -> 'a -> string
val list_transforms : unit -> (string * Pp.formatted) list
val list_transforms_query : 'a -> 'b -> string
val load_strategies : Controller_itp.controller -> unit
val return_prover : string -> Whyconf.config -> Whyconf.config_prover option
type command =
  1. | Transform of string * Trans.gentrans * string list
  2. | Prove of Whyconf.config_prover * Call_provers.resource_limit
  3. | Strategies of string
  4. | Edit of Whyconf.prover
  5. | Bisect
  6. | Replay of bool
  7. | Clean
  8. | Mark_Obsolete
  9. | Focus_req
  10. | Unfocus_req
  11. | Help_message of string
  12. | Query of string
  13. | QError of string
  14. | Other of string * string list
val interp : (string * query) Wstdlib.Hstr.t -> Controller_itp.controller -> Session_itp.any option -> string -> command
val get_first_unproven_goal_around : proved:('a -> bool) -> children:('a -> 'a list) -> get_parent:('a -> 'a option) -> is_goal:('a -> bool) -> is_pa:('a -> bool) -> 'a -> 'a option
OCaml

Innovation. Community. Security.