This package consists of several utility classes for typechecking. The documentation contained in the source files is sufficient for the simpler classes.

The SectTypeEnv class provides convenient methods for adding names with their section and type to the global type environment.

The TypeEnv class provides convenient methods for adding names with their type to the local type environment.

The UnificationEnv class provides convenient methods for maintaining a mapping between a generic/variable type, and the type to which it is unified in a scope, as well as a method for unification of two types. UResult is the result of a unification.

CarrierSet determines the carrier set for a type for re-writing implicit instantiations expressions as explicit instantiations (see Section 13.2.3.2 of the Z standard for details of carrier sets).