1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
\DOC term_unify
\TYPE {term_unify : term list -> term -> term -> instantiation}
\SYNOPSIS
Unify two terms with compatible types
\DESCRIBE
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
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.
\SEEALSO
instantiate, term_match, term_type_unify, type_unify.
\ENDDOC
|
