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)')].