Parameter Make.I

type t

The type of identifiers

type namespace

The type for namespaces.

val var : namespace

Used for type variables.

val term : namespace

Usual namespace, used for terms and propositions.

val sort : namespace

Usual namespace, used for types.

val decl : namespace

Names used to refer to tptp phrases. These are used in declarations and include statement.

val track : namespace

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

val mk : namespace -> string -> t

Make an identifier

val tracked : track:t -> namespace -> string -> t

Make an identifier with an additional name.