Next: Conditional expressions, Previous: Record syntax, Up: Data-terms [Contents]

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.