Unification -- library(unify)

This file defines only one predicate.

unify(?Term1, ?Term2)

is true when Term1 unifies with Term2. The only difference between this predicate and the built-in predicate 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.