Identifiers

In Core Maude, identifiers are the basic syntactic elements, used to name modules and sorts, and to form operator names. For example, NAT, Nat, and hello-world are identifiers. In general, an identifier in Maude is any finite sequence of ASCII characters such that:

• It does not contain any white space. For example, the sequence `abc def' is not one identifier, but two.

• The characters `{', `}', `(', `)', `[', `]' and `,' are special, in that they break a sequence of characters into several identifiers. For example, the sequence ab{c,d}ef counts as seven identifiers, namely, ab, {, c, ,, d, }, and ef.

• The backquote character ``' is used as an escape character to indicate that a blank space or the special characters do not break the sequence. Consequently, backquotes can only appear immediately before any of the special characters, or between two non-empty strings of characters--with neither the ending of the first string nor the beginning of the second string being another backquote--for exactly these purposes. For example, 1`ab`{c`,d`}ef is a single identifier. Maude's pretty printer will display such an identifier in the form 1 ab{c,d}ef.

Nonprinting characters in strings use C backslash conventions [47, Section A2.5.2].