(* and ended by *). Nested comments are handled properly. All comments are ignored
(except in some special case used for TeX generation, see the chapter 9) but like blank they separate adjacent tokens. Strings and characters can use the following escape sequences :
| Sequence | Character denoted |
\n | newline (LF) |
\r | return (CR) |
\t | tabulation (TAB) |
\ddd | The character of code ddd in decimal |
\c | The character c when c is not in 0...9nbt |
| string-character | := | any character but " or an escape sequence. |
| string | := | " {string-character} " |
| char-character | := | any character but ' or an escape sequence. |
| char | := | 'char-character' |
| natural | := | { 0...9 } |
| integer | := | [-] natural |
| float | := | integer [.natural]
[(e E) integer] |
Identifiers are used to give names to mathematical objects. The definition is
more complex than for most programming languages. This is because we want to
have the maximum freedom to get readable files. So for instance the following
are valid identifiers: A_1', <=, <_A. Moreover, in
relation with the module system, identifiers can be prefixed with extension
like in add.assoc or prod.assoc.
| letter | := | A...Za...z |
| end-ident | := | {letter0...9_ } { ' } |
| atom-alpha-ident | := | letterend-ident |
| alpha-ident | := | atom-alpha-ident { .atom-alpha-ident} |
| special-char | := | !%&*+,-/:;<=> |
@[]\#^`\|{}~ | ||
| atom-special-ident | := | {special-char} [_end-ident] |
| special-ident | := | atom-special-ident { .atom-alpha-ident } |
| any-ident | := | alpha-identspecial-ident |
| pattern | := | any-ident (_ {.atom-alpha-ident }) |
| unif-var | := | ? {natural} |
| sort-var | := | ' {letter} |
Exemples:
N, add.commutative.N, x0, x0', x_1 are alpha-idents. <, <<, <_1, +, +_N are special-idents. ?1 is a unif-var. 'a is a sort-var. +, _.N are patterns (used only for renaming
symbol with the module system). The following characters are token by themselves:
().$