Module Wp.Why3ProversSource

Sourceval why3_version : string
Sourceval config : unit -> Why3.Whyconf.config
Sourceval configure : unit -> unit
Sourceval set_procs : int -> unit
Sourcetype t = Why3.Whyconf.prover
Sourceval ident_why3 : t -> string
Sourceval ident_wp : t -> string
Sourceval title : ?version:bool -> t -> string
Sourceval name : t -> string
Sourceval version : t -> string
Sourceval altern : t -> string
Sourceval compare : t -> t -> int
Sourceval lookup : ?fallback:bool -> string -> t option
Sourceval provers : unit -> t list
Sourceval provers_set : unit -> Why3.Whyconf.Sprover.t
Sourceval is_auto : t -> bool
Sourceval is_available : t -> bool
Sourceval is_mainstream : t -> bool
Sourceval has_counter_examples : t -> bool
Sourceval with_counter_examples : t -> t option
Sourcetype model = Why3.Model_parser.concrete_syntax_term