module ProverWhy3: sig
.. end
None if the po is trivial
TODO add them only when needed
type
goal_id = {
|
gfile : string ; |
|
gtheory : string ; |
|
ggoal : string ; |
}
val assemble_wpo : Wpo.t -> (string list * goal_id) option
None if the po is trivial
val prove : Wpo.t -> prover:string -> VCS.result Task.task
The string must be a valid why3 prover identifier
Return NoResult if it is already proved by Qed
val call_ide : includes:string list -> files:string list -> session:string -> bool Task.task
type
dp = {
|
dp_name : string ; |
|
dp_version : string ; |
|
dp_prover : string ; |
}
val detect_why3 : (dp list option -> unit) -> unit
val detect_provers : (dp list -> unit) -> unit
val find : string -> dp list -> dp
val parse : string -> dp