logtk

Core types and algorithms for logic
IN THIS PACKAGE
Module Logtk . Unif_constr

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.

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 with type t := t
val equal : t -> t -> bool
val hash : t -> int
include Interfaces.ORD with type t := t
val compare : t -> t -> int
include Interfaces.PRINT with type t := t
val to_string : t -> string