package term-indexing

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.

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

subst state returns the substitution underlying the unification state.