Module Prover

module Prover: sig .. end
Different instance of why3ide can't be run simultanely

val dispatch : Wpo.t -> VCS.mode -> VCS.prover -> VCS.result Task.task
val qed_time : Wpo.t -> float
val signal : ?callin:('a -> 'b -> unit) -> 'a -> 'b -> unit
val update : ?callback:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->
Wpo.t -> VCS.prover -> VCS.result -> unit
val run_prover : Wpo.t ->
?mode:VCS.mode ->
?callback:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->
VCS.prover -> bool Task.task
val resolve : Wpo.t -> bool
val simplify : ?callin:(Wpo.t -> 'a -> unit) ->
?callback:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->
Wpo.t -> 'a -> bool Task.task
val prove : Wpo.t ->
?mode:VCS.mode ->
?callin:(Wpo.t -> VCS.prover -> unit) ->
?callback:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->
VCS.prover -> bool Task.task
val spawn : Wpo.t ->
?callin:(Wpo.t -> VCS.prover -> unit) ->
?callback:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->
(VCS.mode * VCS.prover) list -> unit
module String: Datatype.String
val why3ide_running : bool Pervasives.ref
Different instance of why3ide can't be run simultanely
val update_wpo_from_session : ?callback:(Wpo.S.Hashtbl.key -> VCS.prover -> VCS.result -> unit) ->
goals:ProverWhy3.goal_id option Wpo.S.Hashtbl.t ->
session:string -> unit -> unit
Update Wpo from Sessions
val wp_why3ide : ?callback:(Wpo.S.Hashtbl.key -> VCS.prover -> VCS.result -> unit) ->
((Wpo.S.Hashtbl.key -> unit) -> 'a) -> unit Task.task
val wp_why3ide : ?callback:(Wpo.S.Hashtbl.key -> VCS.prover -> VCS.result -> unit) ->
((Wpo.S.Hashtbl.key -> unit) -> 'a) -> unit Task.task