term_unify : term list -> term -> term -> instantiation
SYNOPSIS
Unify two terms with compatible types
DESCRIPTION
Given two terms tm1 and tm2, a call term_unify vars tm1 tm2 attempts to
find instantiations of the variables vars in the two terms to make them
alpha-equivalent. The unification is also purely first-order. In these respects
it is less general than term_match, and this may be improved in the future.
FAILURE CONDITIONS
Fails if the two terms are not first-order unifiable by instantiating the given
variables without type instantiation.
COMMENTS
This function is restricted to terms of the same type, but term_type_unify
offers a similar and more general function that handles type differences.