The type of terms

The type of substitutions

state is the type of unification state.

Cannot_unify is raised by unify when a unifier cannot be found.

empty () is an empty unification state.

unify t1 t2 state unifies terms t1 and t2 in state state and returns an updated state.

unify_exn t1 t2 state unifies terms t1 and t2 in state state and returns an updated state.

Raises Cannot_unify if no solution was found.

unify_subst s state unifies s with substitution state state and returns an updated state.

unify_subst s1 s2 state unifies s1 with s2 in state state and returns an updated state.

generalizes t1 t2 checks that there exists a substitution subst such that lift t1 subst = t2.

subst state returns the substitution underlying the unification state.

Occurs_check is raised by unfold when the solution contains a cycle.

unfold state term returns term with variables substituted for their representative terms. Raises Occurs_check if the solution contains a cycle.