Module Logtk.Unif_constrSource

Unification Constraint

A constraint is a pair of (scoped) terms that cannot be unified immediately (because they belong to some theory, for example).

We keep them in a separate constraint that will become a negative literal t ≠ u, on which the theory can then act.

Sourcetype term = InnerTerm.t
Sourcetype t = private {
  1. t1 : term;
  2. sc1 : Scoped.scope;
  3. t2 : term;
  4. sc2 : Scoped.scope;
  5. tags : Proof.tag list;
}

A constraint delayed because unification for this pair of terms is not syntactic

Sourceval make : tags:Proof.tag list -> term Scoped.t -> term Scoped.t -> t
Sourceval tags : t -> Proof.tag list
Sourceval apply_subst : Subst.Renaming.t -> Subst.t -> t -> term * term

Apply a substitution to a delayed constraint

Sourceval apply_subst_l : Subst.Renaming.t -> Subst.t -> t list -> (term * term) list

Apply a substitution to delayed constraints

Sourcemodule FO : sig ... end
include Interfaces.HASH with type t := t
include Interfaces.EQ with type t := t
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
include Interfaces.ORD with type t := t
Sourceval compare : t -> t -> int
include Interfaces.PRINT with type t := t
Sourceval to_string : t -> string