Safe Haskell | None |
---|---|

Language | Haskell98 |

# Documentation

unify :: (Eq f, Ord v) => Term f v -> Term f v -> Maybe (Subst f v) Source #

Unify two terms. If unification succeeds, return a most general unifier of the given terms. We have the following property:

unify t u == Just s ==> apply s t == apply s u

*O(n log(n))*, where *n* is the apparent size of the arguments. Note that
the apparent size of the result may be exponential due to shared subterms.