module Fact: sig end
type t =
type justification =
type equal = Term.t * Term.t * justification option
type diseq = Term.t * Term.t * justification option
type cnstrnt = Term.t * Sign.t * justification option
type rule = string
val mk_axiom : justification option
val mk_rule : string -> justification option list -> justification option
val mk_equal : Term.t -> Term.t -> 'a -> Term.t * Term.t * 'a
val mk_diseq : Term.t -> Term.t -> 'a -> Term.t * Term.t * 'a
val mk_cnstrnt : Term.t -> Sign.t -> 'a -> Term.t * Sign.t * 'a
val d_equal : 'a -> 'a
val d_diseq : 'a -> 'a
val d_cnstrnt : 'a -> 'a
val of_equal : equal -> t
val of_diseq : diseq -> t
val of_cnstrnt : cnstrnt -> t
val pp : Format.formatter -> t -> unit
| Parameters: |
|
fmt |
: |
Format.formatter
|
|
?? |
: |
t
|
|
val pp_equal : Format.formatter -> Term.t * Term.t * 'a -> unit
val pp_diseq : Format.formatter -> Term.t * Term.t * 'a -> unit
val pp_cnstrnt : Format.formatter -> Term.t * Sign.t * 'a -> unit
module Equalset: sig end