module ProverWhy3:sig
..end
type
goal = {
|
file : |
|
theory : |
|
goal : |
val assemble_goal : Wpo.t -> (string list * goal) option
None if the po is trivial
val prove : ?timeout:int -> prover:string -> Wpo.t -> VCS.result Task.task
The string must be a valid why3 prover identifier Return NoResult if it is already proved by Qed
module Goal:sig
..end