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.

Namespace used by modules (for instance in dedulkti).

Make an identifier from its namespace and name.

An identifier with an additional name for tracking purposes.