Module LogtkUnif.HO

module HO: NARY  with type term = LogtkHOTerm.t

type term 
type result = LogtkUnif.res 
val unification : ?env1:LogtkUnif.env ->
?env2:LogtkUnif.env ->
?subst:LogtkUnif.subst ->
term ->
LogtkUnif.scope ->
term -> LogtkUnif.scope -> result
unification of two terms
val matching : ?allow_open:bool ->
?env1:LogtkUnif.env ->
?env2:LogtkUnif.env ->
?subst:LogtkUnif.subst ->
pattern:term ->
LogtkUnif.scope ->
term -> LogtkUnif.scope -> result
matching of two terms.
Raises Invalid_argument if the two scopes are equal.
allow_open : if true, variables can bind to non-closed DB terms (default false)
val variant : ?env1:LogtkUnif.env ->
?env2:LogtkUnif.env ->
?subst:LogtkUnif.subst ->
term ->
LogtkUnif.scope ->
term -> LogtkUnif.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