sig
val ord : unit -> Logtk.Ordering.t
val selection_fun : unit -> Selection.t
val set_selection_fun : Selection.t -> unit
val set_ord : Logtk.Ordering.t -> unit
val signature : unit -> Logtk.Signature.t
val renaming : Logtk.Subst.Renaming.t
val compare : Logtk.Term.t -> Logtk.Term.t -> Logtk.Comparison.t
val select : Selection.t
val lost_completeness : unit -> unit
val is_completeness_preserved : unit -> bool
val add_signature : Logtk.Signature.t -> unit
val find_signature : Logtk.ID.t -> Logtk.Type.t option
val find_signature_exn : Logtk.ID.t -> Logtk.Type.t
val declare : Logtk.ID.t -> Logtk.Type.t -> unit
val on_new_symbol : (Logtk.ID.t * Logtk.Type.t) Logtk.Signal.t
val on_signature_update : Logtk.Signature.t Logtk.Signal.t
module Lit :
sig
val from_hooks : unit -> Logtk.Literal.Conv.hook_from list
val add_from_hook : Logtk.Literal.Conv.hook_from -> unit
val to_hooks : unit -> Logtk.Literal.Conv.hook_to list
val add_to_hook : Logtk.Literal.Conv.hook_to -> unit
val of_form : Logtk.Term.t Logtk.SLiteral.t -> Logtk.Literal.t
val to_form : Logtk.Literal.t -> Logtk.Term.t Logtk.SLiteral.t
end
end