Module `Proof.S`

type t = proof

val result : t -> result
val step : t -> step
val compare : t -> t -> int
val equal : t -> t -> bool
val hash : t -> int
val compare_by_result : t -> t -> int: Compare proofs by their result

module Tbl : CCHashtbl.S with type Tbl.key = t

Constructors and utils

In all the following constructors, theories defaults to the empty list. Axiom constructors have default role "axiom"

val mk : step -> Result.t -> t: Main constructor

val mk_f : step -> form -> t
val mk_f_trivial : form -> t
val mk_f_by_def : ID.t -> form -> t
val mk_f_inference : rule:rule -> form -> parent list -> t
val mk_f_simp : rule:rule -> form -> parent list -> t
val mk_f_esa : rule:rule -> form -> parent list -> t
val adapt : t -> Result.t -> t
val adapt_f : t -> form -> t
val is_proof_of_false : t -> bool

Conversion to a graph of proofs

val as_graph : (t, rule * Subst.Projection.t option * infos) CCGraph.t: Get a graph of the proof

val traverse : ?⁠traversed:unit Tbl.t -> order:[ `BFS | `DFS ] -> t -> t Sequence.t

IO

val pp_result_of : t CCFormat.printer
val pp_notrec : t CCFormat.printer: Non recursive printing on formatter

val pp_notrec1 : t CCFormat.printer: Non recursive printing on formatter, including parents

val pp_tstp : t CCFormat.printer
val pp_normal : t CCFormat.printer
val pp_zf : t CCFormat.printer
val pp_in : Options.print_format -> t CCFormat.printer: Prints the proof according to the given input switch

val pp_dot : name:string -> t CCFormat.printer: Pretty print the proof as a DOT graph

val pp_dot_file : ?⁠name:string -> string -> t -> unit: print to dot into a file

val pp_dot_seq : name:string -> t Sequence.t CCFormat.printer: Print a set of proofs as a DOT graph, sharing common subproofs

val pp_dot_seq_file : ?⁠name:string -> string -> t Sequence.t -> unit: same as pp_dot_seq but into a file