Module Symkat

module Symkat: sig .. end
High-level interface of the library, main entry point for standalone program

val hk : bool Pervasives.ref
do we use Hopcroft and Karp's version?
val congruence : bool Pervasives.ref
do we use up-to congruence
val ssf : bool Pervasives.ref
do we put expressions in strict star form first?
val trace : bool Pervasives.ref
do we trace unifications in Format.str_formatter
val construction : [ `Antimirov | `Brzozowski | `IlieYu ] Pervasives.ref
which construction do we use
val equiv : ?hyps:Hypotheses.t -> Kat.expr -> Kat.expr -> Kat.gstring option
equivalence check, using the above parameters; returns a counter-example if any. If hyps is specified, exploit the corresponding hypotheses (see module Hypotheses).
val compare : ?hyps:Hypotheses.t ->
Kat.expr ->
Kat.expr ->
(Kat.expr' * Kat.expr') *
[ `D of Kat.gstring * Kat.gstring
| `E
| `G of Kat.gstring
| `L of Kat.gstring ]
full comparison: compare ~hyps x y returns
val check : [ `D | `E | `G | `L ] -> ?hyps:string -> string -> string -> unit
utility for verifications: check two expressions for equivalence (`E), difference (`D), left-to-right inclusion (`L), or right-to-left inclusion (`G). Exploit hypotheses if asked to.