package mc2

  1. Overview
  2. Docs

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

Proof exporting

Currently, exporting a proof means printing it into a file according to the conventions of a given format.


module 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


val print : Stdlib.Format.formatter -> Mc2_core.Proof.t -> unit

A function for printing proofs in the desired format.