Needs text improvement

We read:

Finally, if A and B can unify, goals are delayed that prevent A and B to become equal.

This doesn't really make sense to me. There is nothing that is "delayed" really, it's just that a background check is done if A and B are involved in a unification. That description really threw me off.

(With hindsight and after getting into the jargon one realizes that "goals are delayed" might well mean "a procedure will be run asynchronously" ... "to make sure that A and B do not become equal". But a reference manual should not be a grimoire.)

The text in library(dif) is much clearer:

Among the most important coroutining predicates is dif/2, which expresses disequality of terms in a sound way. The actual test is delayed until the terms are sufficiently different, or have become identical.

I prefer to look at it this way:

After a dif(A,B) call, any unification involving A or B or subterms thereof that would make A and B identical (A == B) will fail (and this applies to unification in clause heads, too).

If A and B are already identical at call time, dif(A,B) fails at once.

Writeup on dif

I made a writeup, including examples, here:

About dif/2.

That has turned into a lot of text, hopefully clear.

Note the printing of the "residual goal"

dif/2 prints the "delayed goal" if it is still "live" at query success (the technical for this is "residual goal"):

?- dif(X,a),(X=1;Y=2).

X = 1 ;        % dif/2 constraint cleared
Y = 2,         % dif/2 constraint still live
dif(X, a).     % the residual goal