Parameter Make.I

type t

The type of identifiers

type namespace

Namespace for identifiers

val sort : namespace
val term : namespace
val attr : namespace

The namespace for sorts (also called typee), terms and attributes, respectively.

val mk : namespace -> string -> t

Make an identifier from a name and namespace. Indexed identifiers (which are a list of names), are encoded into a single string with the '\000' character as separator (since it cannot appear in any symbol from smtlib).