The following are the punctuation symbols:
= <> ~= ~<> < <= > >= + - * / -> ( ) { } [ ] " => |=> , $
An identifier is a letter or an underscore followed by any number of letters, digits, or underscores. The case of an identifier is significant.
The following are the keywords. Keywords cannot be used as names of variables or functions.
| and | in | real |
| Boolean | integer | sort |
| current | let | string |
| else | map | then |
| false | model | there_exists |
| filter | not | this |
| for_all | of | traverse |
| if | or | true |
| implies | over |
An integer literal is an optional minus sign followed by one or more decimal digits.
A real literal is an optional minus sign followed by one or more decimal digits, a decimal point, and one or more decimal digits.
The Boolean literals are true and false.
Association literals are essentially string literals with square brackets ([]) in place of quotation marks. The sequence \] escapes the closing delimiter.
A string literal is a sequence of characters enclosed in quotation marks. A string cannot extend across lines (that is, a string cannot contain an unescaped new line). The supported escape sequences are listed in the following table.
A regular expression literal is a sequence of characters enclosed in back quotes. Several characters have special meanings within regular expression literals. These characters have their special meaning unless preceded by a back slash. The special characters are ., \, [, ], ?, *, +, ^, and $. A regular expression literal can contain character escape sequences. The allowed escape sequences are \t, \r, \n, and \xdd, which stand for a tab, a carriage return, a new line, and the character with the ASCII code equal to the hexadecimal number dd.
Regular expressions have a recursive structure. They are formed from smaller subexpressions. The building blocks of all regular expressions are the expressions to match a single character. These fundamental expressions have the following three forms:
From these building blocks, larger regular expressions can be formed in the following way:
A complete regular expression can be anchored to the beginning or end of a string with ^ and $, respectively. If re is a regular expression, then ^re is a regular expression that matches all strings matchable by re but only if they occur at the beginning of a string. Similarly, re$ is a regular expression that matches all strings matchable by re but only if they occur at the end of a string. For example, `^[01]+` matches 0 and 0110 but not a0 or a0110; and `[01]+$` matches 0 and 0110 but not 0a or 0110a.