package why3

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

val get_session_dir : allow_mkdir:bool -> string Queue.t -> string

exception Undefined_id of string

exception Number_of_arguments

type query =

| Qnotask of Controller_itp.controller -> string list -> string
| 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 =

| Transform of string * Trans.gentrans * string list
| Prove of Whyconf.config_prover * Call_provers.resource_limit
| Strategies of string
| Edit of Whyconf.prover
| Get_ce
| Bisect
| Replay of bool
| Clean
| Mark_Obsolete
| Focus_req
| Unfocus_req
| Locate of string
| Help_message of string
| Query of string
| QError of string
| 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