Inferno.OccursCheck
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.