module Wpo: sig
.. end
type
prover
Access it by by writing T.ty
where T
has previously been defined by: let module T = Type.Make(struct let name = Wpo.prover end)
type
result
Access it by by writing T.ty
where T
has previously been defined by: let module T = Type.Make(struct let name = Wpo.result end)
type
po
Access it by by writing T.ty
where T
has previously been defined by: let module T = Type.Make(struct let name = Wpo.po end)
val file_for_log_proof : po -> prover -> string * string
Access it by Dynamic.get ~plugin:"Wp" "Wpo.file_for_log_proof" (Datatype.func Wpo.ty (Datatype.func Wpo.ty (Datatype.pair Datatype.string Datatype.string)))
val prover_of_name : string -> prover option
Access it by Dynamic.get ~plugin:"Wp" "Wpo.prover_of_name" (Datatype.func Datatype.string (Datatype.option Wpo.ty))
val iter_on_goals : (po -> unit) -> unit
Access it by Dynamic.get ~plugin:"Wp" "Wpo.iter_on_goals" (Datatype.func (Datatype.func Wpo.ty Datatype.unit) Datatype.unit)
val is_valid : result -> bool
Access it by Dynamic.get ~plugin:"Wp" "Wpo.is_valid" (Datatype.func Wpo.ty Datatype.bool)
val goals_of_property : Property.t -> po list
Access it by Dynamic.get ~plugin:"Wp" "Wpo.goals_of_property" (Datatype.func Property.ty (Datatype.list Wpo.ty))
val get_result : po ->
prover -> result
Access it by Dynamic.get ~plugin:"Wp" "Wpo.get_result" (Datatype.func Wpo.ty (Datatype.func Wpo.ty Wpo.ty))
val get_gid : po -> string
Access it by Dynamic.get ~plugin:"Wp" "Wpo.get_gid" (Datatype.func Wpo.ty Datatype.string)
val get_property : po -> Property.t
Access it by Dynamic.get ~plugin:"Wp" "Wpo.get_property" (Datatype.func Wpo.ty Property.ty)