package why3

  1. Overview
  2. Docs
package why3
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.

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