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

is that the expression is replaced by a
fresh variable `X` @ `Y``Z`

, and immediately after `Z`

is evaluated,
the conjunction `Z = `

is evaluated.
`X`, Z = `Y`

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.