package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

Unification Substitution

A tuple for full-unification, containing:

  • the substitution itself
  • delayed constraints (if any)
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 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct