Module Inferno.OccursCheck

module Make (S : sig ... end) (U : sig ... end) : sig ... end

This module traverses the data structure maintained by the unifier and offers an occurs check, that is, a cycle detection algorithm. It is parameterized by the term structure S and by the unifier U. Read-only access to the unifier's data structure suffices.