Functor Ctx.Make

module Make: 
functor (X : PARAMETERS) -> S

Create a new context


Parameters:
X : PARAMETERS

val ord : unit -> Logtk.Ordering.t
current ordering on terms
val selection_fun : unit -> Selection.t
selection function for clauses
val set_selection_fun : Selection.t -> unit
val set_ord : Logtk.Ordering.t -> unit
val signature : unit -> Logtk.Signature.t
Current signature
val renaming : Logtk.Subst.Renaming.t

Utils


val compare : Logtk.Term.t -> Logtk.Term.t -> Logtk.Comparison.t
Compare two terms
val select : Selection.t
val lost_completeness : unit -> unit
To be called when completeness is not preserved
val is_completeness_preserved : unit -> bool
Check whether completeness was preserved so far
val add_signature : Logtk.Signature.t -> unit
Merge the given signature with the context's one
val find_signature : Logtk.ID.t -> Logtk.Type.t option
Find the type of the given symbol
val find_signature_exn : Logtk.ID.t -> Logtk.Type.t
Unsafe version of Ctx_intf.S.find_signature.
Raises Not_found for unknown symbols
val declare : Logtk.ID.t -> Logtk.Type.t -> unit
Declare the type of a symbol (updates signature)
val on_new_symbol : (Logtk.ID.t * Logtk.Type.t) Logtk.Signal.t
val on_signature_update : Logtk.Signature.t Logtk.Signal.t

Literals


module Lit: sig .. end