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
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 locate_id : 'a -> Trans.naming_table -> string list -> Loc.position option
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. | Get_ce
  6. | Bisect
  7. | Replay of bool
  8. | Clean
  9. | Mark_Obsolete
  10. | Focus_req
  11. | Unfocus_req
  12. | Locate of string
  13. | Help_message of string
  14. | Query of string
  15. | QError of string
  16. | Other of string * string list
val interp : (string * query) Wstdlib.Hstr.t -> Controller_itp.controller -> Session_itp.any option -> string -> command
val get_next_with_strategy : st:Itp_communication.next_unproved_node_strat -> always_send:bool -> 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.