term_type_unify : term -> term -> instantiation -> instantiation
- SYNOPSIS
-
Unify two terms including their type variables
- DESCRIPTION
-
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 CONDITIONS
-
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.
- SEE ALSO
-
instantiate, term_match, term_unify, type_unify.