package logtk

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Proof.SSource

Sourcetype t = proof
Sourceval result : t -> result
Sourceval step : t -> step
Sourceval compare : t -> t -> int
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
Sourceval compare_by_result : t -> t -> int

Compare proofs by their result

Sourcemodule Tbl : CCHashtbl.S with type key = t

Constructors and utils

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

Sourceval mk : step -> Result.t -> t

Main constructor

Sourceval mk_f : step -> form -> t
Sourceval mk_f_trivial : form -> t
Sourceval mk_f_by_def : ID.t -> form -> t
Sourceval mk_f_inference : rule:rule -> form -> parent list -> t
Sourceval mk_f_simp : rule:rule -> form -> parent list -> t
Sourceval mk_f_esa : rule:rule -> form -> parent list -> t
Sourceval adapt : t -> Result.t -> t
Sourceval adapt_f : t -> form -> t
Sourceval is_proof_of_false : t -> bool
Conversion to a graph of proofs
Sourceval as_graph : (t, rule * Subst.Projection.t option * infos) CCGraph.t

Get a graph of the proof

Sourceval traverse : ?traversed:unit Tbl.t -> order:[ `BFS | `DFS ] -> t -> t Iter.t
IO
Sourceval pp_result_of : t CCFormat.printer
Sourceval pp_notrec : t CCFormat.printer

Non recursive printing on formatter

Sourceval pp_notrec1 : t CCFormat.printer

Non recursive printing on formatter, including parents

Sourceval pp_normal : t CCFormat.printer

Prints the proof according to the given input switch

Sourceval pp_dot : name:string -> t CCFormat.printer

Pretty print the proof as a DOT graph

Sourceval pp_dot_file : ?name:string -> string -> t -> unit

print to dot into a file

Sourceval pp_dot_seq : name:string -> t Iter.t CCFormat.printer

Print a set of proofs as a DOT graph, sharing common subproofs

Sourceval pp_dot_seq_file : ?name:string -> string -> t Iter.t -> unit

same as pp_dot_seq but into a file

OCaml

Innovation. Community. Security.