package why3find

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

type status = private

and crc = private {

}

val none : status

val stuck : ?goal:Session.goal -> unit -> crc

val prover : ?goal:Session.goal -> Prover.desc -> float -> crc

val tactic : ?goal:Session.goal -> Tactic.tactic -> crc list -> crc

val iter : (Session.goal -> status -> unit) -> crc -> unit

Iterates over all goals in the CRC. Tactic nodes are visite first, followed by their children.

type verdict = [

]

val verdict : crc -> verdict

val verdict_all : crc list -> verdict

val nverdict : stuck:int -> proved:int -> verdict

val get_stuck : crc -> int

val get_proved : crc -> int

val get_time : crc -> float

val get_depth : crc -> int

val size : crc -> int

val get_stuck_all : crc list -> int

val get_proved_all : crc list -> int

val get_time_all : crc list -> float

val get_depth_all : crc list -> int

val is_stuck : crc -> bool

val is_unknown : crc -> bool

val is_complete : crc -> bool

val pretty : Format.formatter -> crc -> unit

val pp_status : Format.formatter -> status -> unit

val pp_result : Format.formatter -> stuck:int -> proved:int -> unit

val dump : Format.formatter -> crc -> unit

val merge : crc -> crc -> crc

val of_json : Why3findUtils.Json.t -> crc

val to_json : crc -> Why3findUtils.Json.t