package symkat

  1. Overview
  2. Docs
val hk : bool Stdlib.ref
val congruence : bool Stdlib.ref
val ssf : bool Stdlib.ref
val trace : bool Stdlib.ref
val construction : [ `Antimirov | `Brzozowski | `IlieYu ] Stdlib.ref
val equiv : ?hyps:Hypotheses.t -> Kat.expr -> Kat.expr -> Kat.gstring option
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 ]
val check : [ `D | `E | `G | `L ] -> ?hyps:string -> string -> string -> unit