2.15.3 Unification expressions

A unification expression is an expression of the form

X @ Y

where X and Y are data-terms.

The meaning of a unification expression is that the arguments are unified, and the expression is equivalent to the unified value.

The strict sequential operational semantics (see Semantics) of an expression X @ Y is that the expression is replaced by a fresh variable Z, and immediately after Z is evaluated, the conjunction Z = X, Z = Y is evaluated.

For example

p(X @ f(_, _), X).

is equivalent to

p(H1, H2) :-
    H1 = X,
    H1 = f(_, _),
    H2 = X.

Unification expressions are most useful when writing switches (see Determinism checking and inference). The arguments of a unification expression are examined when checking for switches. The arguments of an equivalent user-defined function would not be.