[ Comparing and Sorting | The ECLiPSe Built-In Predicates | 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.

Fail Conditions

Fails if Term1 and Term2 can be unified.

Resatisfiable

No.

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