Functor Dot.Simple

module Simple: functor (S : Res.S) -> functor (A : Arg  with type atom := S.St.formula
                                  and type hyp = S.St.formula list
                                  and type lemma := S.lemma
                                  and type assumption = S.St.formula) -> S  with type t := S.proof

Functor for making a module to export proofs to the DOT format. The substitution of the hyp type is non-destructive due to a restriction of destructive substitutions on earlier versions of ocaml.

Parameters:

`S`	:	`Res.S`
`A`	:	`Arg with type atom := S.St.formula and type hyp = S.St.formula list and type lemma := S.lemma and type assumption = S.St.formula`

Proof exporting

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

type t

The type of proofs.

val print : Format.formatter -> t -> unit

A function for printing proofs in the desired format.