module Fact: sig end
Datatype of facts (justified atoms)
Author(s): Harald Ruess
type t = Atom.t * Jst.t
A fact is an atom together with a justification (proof) of this
atom in terms of axioms.
val pp : t Pretty.printer
Pretty-printing the atom of a justification. In case
Fact.print_justification
is set, this also prints the justification.
val print_justification : bool Pervasives.ref
Fact.pp prints justification only if this flag is set to
true.
val eq : t -> t -> bool
val map : Jst.Eqtrans.t -> t -> t
val replace : Term.t * Term.t * Jst.t -> t -> t
module Equal: sig end
Equality Facts
module Diseq: sig end
Disequality Facts
module Nonneg: sig end
Nonnegativity facts
module Pos: sig end
Nonnegativity facts
val of_equal : Equal.t -> t
val of_diseq : Diseq.t -> t