Dot (p.mc2.0.1.doc.mc2.backend.Mc2

Dot backend for proofs

This module provides functions to export proofs into the dot graph format. Graphs in dot format can be used to generates images using the graphviz tool.

Sourcemodule type S = Backend_intf.S

Interface for exporting proofs.

Sourcemodule type Arg = sig ... end

Term printing for DOT

Source

module Default : 
  Arg
    with type atom := Mc2_core.Atom.t
     and type hyp := Mc2_core.Clause.t
     and type lemma := Mc2_core.Clause.t
     and type assumption := Mc2_core.Clause.t

Provides a reasonnable default to instantiate the Make functor, assuming the original printing functions are compatible with DOT html labels.

Source

module Make
  (A : 
    Arg
      with type atom := Mc2_core.Atom.t
       and type hyp := Mc2_core.Clause.t
       and type lemma := Mc2_core.Clause.t
       and type assumption := Mc2_core.Clause.t) : 
  S with type t := Mc2_core.Proof.t

Functor for making a module to export proofs to the DOT format.