Module Env.ProofState
module Ctx = Ctx
module C = C
Useful Index structures
module TermIndex : Logtk.Index.TERM_IDX with type elt = C.WithPos.t
module UnitIndex : Logtk.Index.UNIT_IDX with type E.t = Logtk.Term.t * Logtk.Term.t * bool * C.t and type E.rhs = Logtk.Term.t
module SubsumptionIndex : Logtk.Index.SUBSUMPTION_IDX with type C.t = C.t
Common Interface for Sets
module type CLAUSE_SET = sig ... end
module ActiveSet : sig ... end
module SimplSet : CLAUSE_SET
module PassiveSet : sig ... end
Misc
val stats : unit -> stats
Compute statistics