1.1 Lexical conventions
Blanks
Space, newline and horizontal tabulation are considered as blanks. Blanks are ignored but they separate tokens.Comments
Comments in Coq are enclosed between (* and *), and can be nested. Comments are treated as blanks.Identifiers
Identifiers, written ident, are sequences of letters, digits,_, $
and ', that do not start with a digit or '. That is,
they are recognized by the following lexical class:| first_letter | ::= | a..z | A..Z | _ | $ |
| subsequent_letter | ::= | a..z | A..Z | 0..9 | _ | $ | ' |
| ident | ::= | first_letter[subsequent_letter...subsequent_letter] |
Natural numbers and integers
Numerals are sequences of digits. Integers are numerals optionally preceded by a minus sign.| digit | ::= | 0..9 |
| num | ::= | digit...digit |
| integer | ::= | [-]num |
Strings
Strings are delimited by" (double quote), and enclose a
sequence of any characters different from " and \, or
one of the following sequences
| Sequence | Character denoted |
\\ |
backslash (\) |
\" |
double quote (") |
\n |
newline (LF) |
\r |
return (CR) |
\t |
horizontal tabulation (TAB) |
\b |
backspace (BS) |
\ddd |
the character with ASCII code ddd in decimal |
\) at
the end of each line, just before the newline. For instance,AddPath "$COQLIB/\ contrib/Rocq/LAMBDA".
Coq < AddPath "$COQLIB/contrib/Rocq/LAMBDA".Keywords
The following identifiers are reserved keywords, and cannot be employed otherwise:
as |
end |
in |
of |
using |
with |
Axiom |
Cases |
CoFixpoint |
CoInductive |
Compile |
Definition |
Fixpoint |
Grammar |
Hypothesis |
Inductive |
Load |
Parameter |
Proof |
Prop |
Qed |
Quit |
Set |
Syntax |
Theorem |
Type |
Variable |
Although they are not considered as keywords, it is not advised to use words of the following list as identifiers:
Add |
AddPath |
Abort |
Abstraction |
All |
Begin |
Cd |
Chapter |
Check |
Compute |
Defined |
DelPath |
Drop |
End |
Eval |
Extraction |
Fact |
Focus |
Goal |
Guarded |
Hint |
Immediate |
Induction |
Infix |
Inspect |
Lemma |
Let |
LoadPath |
Local |
Minimality |
ML |
Module |
Modules |
Mutual |
Opaque |
Parameters |
Print |
Pwd |
Remark |
Remove |
Require |
Reset |
Restart |
Restore |
Resume |
Save |
Scheme |
Search |
Section |
Show |
Silent |
State |
States |
Suspend |
Syntactic |
Test |
Transparent |
Undo |
Unset |
Unfocus |
Variables |
Write |
Special tokens
The following sequences of characters are special tokens:
| |
: |
:= |
= |
> |
>> |
<> |
<< |
< |
-> |
; |
# |
* |
, |
? |
@ |
:: |
/ |
<- |
=> |
Lexical ambiguities are resolved according to the ``longest match'' rule: when a sequence of non alphanumerical characters can be decomposed into several different ways, then the first token is the longest possible one (among all tokens defined at this moment), and so on.