Module `Logtk.Unif_subst`

Unification Substitution

type term = Subst.term
type var = Subst.var
type t

val empty : t: Empty

val is_empty : t -> bool: Both substitution and constraints are empty

val subst : t -> Subst.t: Substitution

val constr_l : t -> Unif_constr.t list: Constraints

val constr_l_subst : Subst.Renaming.t -> t -> (term * term) list: Apply the substitution to the constraint

val tags : t -> Proof.tag list
val has_constr : t -> bool: Is there any constraint?

val make : Subst.t -> Unif_constr.t list -> t
val of_subst : Subst.t -> t
val map_subst : f:(Subst.t -> Subst.t) -> t -> t
val add_constr : Unif_constr.t -> t -> t
val deref : t -> term Scoped.t -> term Scoped.t
val bind : t -> var Scoped.t -> term Scoped.t -> t
val update : t -> var Scoped.t -> term Scoped.t -> t
val mem : t -> var Scoped.t -> bool
val merge : t -> t -> t
val compose : scope:Scoped.scope -> t -> t -> t

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