The function ` unify` is a unification
function
for terms. This
function takes two terms and produces the most general unifier (a
substitution) such that if a ` replace`
is performed on each of the terms using
the unifier, the result is the same term. The unification function fails if
there is no unifier. This function provides a simple way to decompose
terms without using the term destructors. The only variables that will be
substituted for are those
whose names are preceded by an underscore,
e.g., ``` _meta`''. For example,

unify 'x:int#(x=x in int)' '_var:_left_type#_right_type'

results in the unifier

[('_var', 'x'); ('_left_type', 'int'); ('_right_type', '(x=x in int)')].

Thu Sep 14 08:45:18 EDT 1995