[ Comparing and Sorting | Reference Manual | Alphabetic Index ]

not_unify(?Term1, ?Term2)

Succeeds if Term1 and Term2 are not unifiable.
Term1
An arbitrary term.
Term2
An arbitrary term.

Description

Succeeds if Term1 and Term2 are not unifiable. This predicate differs from \=/2 only if attributed variables are involved (e.g. with delayed goals or constraints). While \=/2 does unification, waking of delayed goals and full constraint propagation to determine unifiability, not_unify/2 uses the test_unify-handler for this purpose. not_unify/2 is therefore likely to be cheaper, but possibly less precise (depending on the test_unify-handler) than \=/2.

Modes and Determinism

Fail Conditions

Fails if Term1 and Term2 can be unified.

Examples

Success:
   not_unify(atom, neutron).
   not_unify(1.0, 1).
Fail:
   not_unify(X, Y).
   not_unify(X, 1).
Note the difference:
   coroutine, X > 1, X \= 1.
       % succeeds because the delayed goal X>1 is
       % taken into account
   coroutine, X > 1, not_unify(X, 1).
       % fails because the delayed goal X>1 is
       % ignored by the test_unify handler



See Also

= / 2, \= / 2, \== / 2, meta_attribute / 2