Module Logtk.Unif_constr

Unification Constraint

type term = InnerTerm.t
type t = private {
t1 : term;
sc1 : Scoped.scope;
t2 : term;
sc2 : Scoped.scope;
tags : Proof.tag list;
}

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

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

Apply a substitution to a delayed constraint

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

Apply a substitution to delayed constraints

module FO : sig ... end
include Interfaces.HASH with type t := t
include Interfaces.EQ
type t
val equal : t -> t -> bool
val hash : t -> int
include Interfaces.ORD with type t := t
type t
val compare : t -> t -> int
include Interfaces.PRINT with type t := t
type t
val pp : t CCFormat.printer
val to_string : t -> string