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
X @ Y is that the expression is replaced by a
fresh variable Z, and immediately after Z is evaluated,
Z = X, Z = Y is evaluated.
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.