[ Comparing and Sorting | Reference Manual | Alphabetic Index ]

?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. It is implemented like 

    X \= X :- true, !, fail.
    _ \= _.
I.e. the arguments are unified, which may cause delayed goals to be woken and constraints to be checked. Only if all this succeeds, \=/2 fails.

This predicate has a negation-as-failure semantics and so if the compared terms are not ground, it may give unexpected results. Note that the original arguments are unchanged after the predicate succeeds.

Modes and Determinism

Fail Conditions

Fails if Term1 and Term2 can be unified.

Examples

Success:
   atom \= neutron.
   1.0 \= 1.
   f(1,2) \= f(1,3).
   [1,2] \= [1,3].
   [a,b,c] \= [a,b|c].
   [a,b,c] \= [X].
   [a,X,c,Y] \= [X,b,Y,d].
   coroutine, X > 1, X \= 1.
Fail:
   X \= Y.
   1 \= X.
   [a,b|X] \= X.

See Also

= / 2, \== / 2, not_unify / 2