Module Wp.Prover

module Prover: sig .. end

val simplify : ?start:(Wp.Wpo.t -> unit) ->
?result:(Wp.Wpo.t -> Wp.VCS.prover -> Wp.VCS.result -> unit) ->
Wp.Wpo.t -> bool Task.task
val prove : Wp.Wpo.t ->
?config:Wp.VCS.config ->
?mode:Wp.VCS.mode ->
?start:(Wp.Wpo.t -> unit) ->
?progress:(Wp.Wpo.t -> string -> unit) ->
?result:(Wp.Wpo.t -> Wp.VCS.prover -> Wp.VCS.result -> unit) ->
Wp.VCS.prover -> bool Task.task
val spawn : Wp.Wpo.t ->
delayed:bool ->
?config:Wp.VCS.config ->
?start:(Wp.Wpo.t -> unit) ->
?progress:(Wp.Wpo.t -> string -> unit) ->
?result:(Wp.Wpo.t -> Wp.VCS.prover -> Wp.VCS.result -> unit) ->
?success:(Wp.Wpo.t -> Wp.VCS.prover option -> unit) ->
?pool:Task.pool -> (Wp.VCS.mode * Wp.VCS.prover) list -> unit