module Wpo: sig
.. end
type
prover
Access it by by writing T.ty
where T
has previously been defined by: module T = Type.Abstract(struct let name = Wpo.prover end)
. Be careful to replace occurrences of Wpo.prover by T.ty anywhere else in this doc.
type
result
Access it by by writing T.ty
where T
has previously been defined by: module T = Type.Abstract(struct let name = Wpo.result end)
. Be careful to replace occurrences of Wpo.result by T.ty anywhere else in this doc.
type
po
Access it by by writing T.ty
where T
has previously been defined by: module T = Type.Abstract(struct let name = Wpo.po end)
. Be careful to replace occurrences of Wpo.po by T.ty anywhere else in this doc.
val file_for_log_proof : po -> prover -> string * string
Access it by Dynamic.get ~plugin:"Wp" "Wpo.file_for_log_proof" (Datatype.func Wpo.po (Datatype.func Wpo.prover (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.prover))
val iter_on_goals : (po -> unit) -> unit
Access it by Dynamic.get ~plugin:"Wp" "Wpo.iter_on_goals" (Datatype.func (Datatype.func Wpo.po Datatype.unit) Datatype.unit)
val is_valid : result -> bool
Access it by Dynamic.get ~plugin:"Wp" "Wpo.is_valid" (Datatype.func Wpo.result 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.po))
val get_result : po ->
prover -> result
Access it by Dynamic.get ~plugin:"Wp" "Wpo.get_result" (Datatype.func Wpo.po (Datatype.func Wpo.prover Wpo.result))
val get_gid : po -> string
Access it by Dynamic.get ~plugin:"Wp" "Wpo.get_gid" (Datatype.func Wpo.po Datatype.string)
val get_property : po -> Property.t
Access it by Dynamic.get ~plugin:"Wp" "Wpo.get_property" (Datatype.func Wpo.po Property.ty)