This section defines the lexical syntax of WORDS,
DOT-WORDS, NO-BRACKET-
SIGNS, DIGIT,
DIGITS, NUMBER, and QUOTED-CHAR, which are used
in Section C.2, together with that of
FRACTION, FLOATING, and STRING, which are used in
Section C.6. The lexical syntax of URL and
PATH has not yet been finalized, and is left open.
Spaces and other layout characters terminate lexical symbols (except for QUOTED-CHAR and STRING) and are otherwise ignored. The next lexical symbol recognized is as long as possible.
A WORDS must start with a LETTER, and must not be one of the reserved keywords used in the context-free syntax in Section C.2. The (51) keywords are:WORDS ::= WORD _..._ WORD DOT-WORDS ::= . WORDS WORD ::= LETTER-P-D ... LETTER-P-D LETTER-P-D ::= LETTER | "'" | DIGIT LETTER ::= A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | a | b | c | d | e | f | g | h | i | j | k | l | m | n | o | p | q | r | s | t | u | v | w | x | y | z | À | Á | Â | Ã | Ä | Å | Æ | Ç | È | É | Ê | Ë | Ì | Í | Î | Ï | Ñ | Ò | Ó | Ô | Õ | Ö | Ø | Ù | Ú | Û | Ü | Ý | ß | à | á | â | ã | ä | å | æ | ç | è | é | ê | ë | ì | í | î | ï | ñ | ò | ó | ô | õ | ö | ø | ù | ú | û | ü | ý | ÿ DIGIT ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 DIGITS ::= DIGIT DIGIT ... DIGIT NUMBER ::= DIGIT | DIGITS
LETTER includes all the ISO Latin-1 national and accented letters except for the Icelandic `eth' and `thorn'.and arch as assoc axiom axioms closed comm def else end exists false fit forall free from generated get given hide idem if in lambda library local not op ops pred preds result reveal sort sorts spec then to true type types unit units var vars version view when with within .
A NO-BRACKET-SIGNS must not be one of the following reserved symbols:NO-BRACKET-SIGNS ::= NO-BRACKET-SIGN ... NO-BRACKET-SIGN
These sequences of characters may however be used together with other characters in a NO-BRACKET-SIGNS. For example, `==', `:=', and `||' is each recognized as a complete NO-BRACKET-SIGNS. Note that identifiers that start or finish with a NO-BRACKET-SIGNS need to be separated by (e.g.) a space from adjacent reserved symbols: a sequence of characters such as ` #: ' is always recognized as a single symbol, whereas ` # : ' is recognized as two symbols.: :? ::= = => <=> . · | |-> \/ /\ ¬
Despite its use in the context-free syntax as a terminal symbol, a single character `<', `*', `?', `!', or `/' is also recognized as a complete NO-BRACKET-SIGNS. The ISO Latin-1 characters for product `×', negation `¬ ', and raised dot `·' are recognized as alternatives for the terminal symbols `*', `not', and `.', respectively.
Note that NO-BRACKET-SIGN does not include the following ASCII signs:NO-BRACKET-SIGN ::= + | - | * | / | \ | & | = | < | > | ! | ? | : | . | $ | @ | # | ^ | ~ | !` | ?` | × | ÷ | £ | © | ± | ¶ | § | ¹ | ² | ³ | · | ¢ | ° | ¬ | µ | "|"
nor the ISO Latin-1 signs for general currency, yen, broken vertical bar, registered trade mark, masculine and feminine ordinals, left and right angle quotes, fractions, soft hyphen, acute accent, cedilla, macron, and umlaut.( ) [ ] { } ; , ` " %
Pairs of single quotes `'...'' (with no spaces between them) are used in the above productions to indicate symbols containing the double quote character `"', and vice versa.QUOTED-CHAR ::= "'" CHAR "'" CHAR ::= " " | ! | '\"' | # | $ | ... | "\'" | ... | "\\" | ... | \n | \t | \r | ... | \000 ... | \255 FRACTION ::= NUMBER . NUMBER FLOATING ::= NUMBER "E" OPT-SIGN NUMBER | FRACTION "E" OPT-SIGN NUMBER OPT-SIGN ::= + | - | STRING ::= '"' '"' | '"' CHAR ... CHAR '"'