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.