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_type_unify
\TYPE {term_type_unify : term -> term -> instantiation -> instantiation}
\SYNOPSIS
Unify two terms including their type variables
\DESCRIBE
Given two terms {tm1} and {tm2} and an existing instantiation {i} of type and
term variables, a call {term_type_unify tm1 tm2 i} attempts to find an
augmentation of the instantiation {i} that makes the terms alpha-equivalent.
The unification is purely first-order.
\FAILURE
Fails if the two terms are not first-order unifiable by instantiating the given
variables and type variables.
\COMMENTS
The more restrictive {term_unify} does a similar job when the type variables
are already compatible and only terms need to be instantiated.
\SEEALSO
instantiate, term_match, term_unify, type_unify.
\ENDDOC
|
