Module Inferno.Structure

This functor transforms a type 'a structure, equipped with map, iter and conjunction operations, into the type 'a structure option, equipped with the same operations. The type 'a structure option is typically useful when implementing some form of unification of terms: indeed, the optional structure None indicates the absence of a constraint, while the optional structure Some term indicates the presence of an equality constraint.