The type of identifiers.

The type of namespaces. Namespaces are used to distinguish identifiers with the same name, but that occur in different contexts. For instance, in smtlib, sorts and terms live in different namespaces; so a term constant can have the same name as a sort, and still be syntactically different.

The namespace for sorts (also called types). Currently only used for smtlib.

Namespace for variables (when they can be syntatically distinguished from constants).

The usual namespace for terms.

Namespace used for attributes (also called annotations) in smtlib.

Namespace used for declaration identifiers (for instance used to filter declarations during includes)

Namespace used to tag and identify sub-terms occuring in files.

Make an identifier from its namespace and name.

Make an indexed identifier from a namespace, basename and list of indexes.

Make a qualified identifier from a namespace, a list of modules (a path), and a base name.

An identifier with an additional name for tracking purposes.