library(unify)
This file defines only one predicate.
unify(
?Term1,
?Term2)
Term1 =
Term2
is
that unify/2
applies the "occur check" and the built-in predicate =/2
does not. This means that according to ordinary logic,
a variable X should not unify with a term containing X. unify/2
does this correctly and =/2
does not. Thus
| ?- unify(X, [X]). no | ?- X = [X]. X = [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[...
Whenever unify(X, Y)
succeeds, X = Y
would have succeeded and
made the same variable bindings.