LP, the Larch Prover — Symbols
LP divides its input into a sequence of symbols (also known as
tokens) of the following kinds.
Simple identifiers
A <simpleId> is a string of letters, digits, apostrophes, and underscores.
Exceptions: a <simpleId> cannot consist of an underscore or an apostrophe
alone, and it cannot contain two adjacent underscores. Examples: Nat,
10, x', a_1.
A <number> is a <simpleId> consisting entirely of digits. See also
keyword.
Operator identifiers
An <opId> is a string of operator characters, that is, characters
chosen from among "!#$&*+-./<=>?@^|~", or it is the special symbol "/\".
Exception: The symbol -> is not an <opId>. Examples: +, ~=,
<=>.
Escaped identifiers
An <escapedId> consists of the escape character "\" alone or the
escape character followed by a simple identifier, an operator character, an
underscore, another escape character, or a punctuation mark. Examples:
\in, \-, \_, \\, \(.
Punctuation marks
Each of the characters in ":,;()[]{}%" is a separate token, unless it is
immediately preceded by the escape character. The marker symbol "__"
is also treated as a punctuation mark.
Whitespace
A space, tab, or newline terminates the preceding token and is otherwise
ignored. Likewise, all characters from an unescaped percent sign through the
following newline are treated as whitespace. See the comment command.
Illegal characters
The characters """ and "`", as well as all control characters other than
whitespace, are reserved for future use. They should not appear in LP scripts
except within comments.
Strings
In certain contexts, LP reads its input without dividing it into tokens. A
<string> is an arbitrary sequence of characters other than newlines. A
<blank-free-string> is a <string> that does not contain any whitespace.