package logtk

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type term
type result = res
val unification : ?env1:env -> ?env2:env -> ?subst:subst -> term -> scope -> term -> scope -> result

unification of two terms

val matching : ?allow_open:bool -> ?env1:env -> ?env2:env -> ?subst:subst -> pattern:term -> scope -> term -> scope -> result

matching of two terms.

  • parameter allow_open

    if true, variables can bind to non-closed DB terms (default false)

  • raises Invalid_argument

    if the two scopes are equal.

val variant : ?env1:env -> ?env2:env -> ?subst:subst -> term -> scope -> term -> scope -> result

alpha-equivalence checking of two terms

val are_unifiable : term -> term -> bool
val matches : pattern:term -> term -> bool
val are_variant : term -> term -> bool