If X
can be matched with Y
the goal succeeds else the goal fails. A X==Y
goal will only consider an uninstantiated variable to be equal to another uninstantiated variable that is already sharing with it.
Examples
?- X == Y.
no
?- _ == _.
no
?- X == X.
X = UNINSTANTIATED VARIABLE
yes
?- _1 == _1.
_1 = UNINSTANTIATED VARIABLE
yes
?- X = Y, X == Y, Y = 1.
X = 1
Y = 1
yes
?- X == Y, Y = 1, X = Y.
no
?- a=a.
yes
?- 1=1.
yes
?- 1.0=1.0.
yes
?- 1=1.0.
no
?- '+'(1,2)=1+2.
yes
?- append([A|B],C) == append(X,Y).
no
?- append([A|B],C) == append([A|B],C).
A = UNINSTANTIATED VARIABLE
B = UNINSTANTIATED VARIABLE
C = UNINSTANTIATED VARIABLE
yes