next up previous contents index
Next: Example Tactics Up: Tools for Tactic Previous: Substitution


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

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995