package logtk

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Logtk.Unif_substSource

Unification Substitution

A tuple for full-unification, containing:

  • the substitution itself
  • delayed constraints (if any)
Sourcetype term = Subst.term
Sourcetype var = Subst.var
Sourcetype t
Sourceval empty : t

Empty

Sourceval is_empty : t -> bool

Both substitution and constraints are empty

Sourceval subst : t -> Subst.t

Substitution

Sourceval constr_l : t -> Unif_constr.t list

Constraints

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

Apply the substitution to the constraint

Sourceval tags : t -> Proof.tag list
Sourceval has_constr : t -> bool

Is there any constraint?

Sourceval make : Subst.t -> Unif_constr.t list -> t
Sourceval of_subst : Subst.t -> t
Sourceval map_subst : f:(Subst.t -> Subst.t) -> t -> t
Sourceval add_constr : Unif_constr.t -> t -> t
Sourceval deref : t -> term Scoped.t -> term Scoped.t
Sourceval bind : t -> var Scoped.t -> term Scoped.t -> t
Sourceval update : t -> var Scoped.t -> term Scoped.t -> t
Sourceval mem : t -> var Scoped.t -> bool
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
OCaml

Innovation. Community. Security.