1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
.. _lexical-conventions:
Lexical conventions
===================
Blanks
Space, newline and horizontal tab are considered blanks.
Blanks are ignored but they separate tokens.
Comments
Comments are enclosed between ``(*`` and ``*)``. They can be nested.
They can contain any character. However, embedded :n:`@string` literals must be
correctly closed. Comments are treated as blanks.
Identifiers
Identifiers, written :n:`@ident`, are sequences of letters, digits, ``_`` and
``'``, that do not start with a digit or ``'``. That is, they are
recognized by the following grammar (except that the string ``_`` is reserved;
it is not a valid identifier):
.. insertprodn ident subsequent_letter
.. prodn::
ident ::= @first_letter {* @subsequent_letter }
first_letter ::= {| a .. z | A .. Z | _ | @unicode_letter }
subsequent_letter ::= {| @first_letter | @digit | ' | @unicode_id_part }
All characters are meaningful. In particular, identifiers are case-sensitive.
:production:`unicode_letter` non-exhaustively includes Latin,
Greek, Gothic, Cyrillic, Arabic, Hebrew, Georgian, Hangul, Hiragana
and Katakana characters, CJK ideographs, mathematical letter-like
symbols and non-breaking space. :production:`unicode_id_part`
non-exhaustively includes symbols for prime letters and subscripts.
Numerals
Numerals are sequences of digits with an optional fractional part
and exponent, optionally preceded by a minus sign. :n:`@int` is an integer;
a numeral without fractional or exponent parts. :n:`@num` is a non-negative
integer. Underscores embedded in the digits are ignored, for example
``1_000_000`` is the same as ``1000000``.
.. insertprodn numeral digit
.. prodn::
numeral ::= {+ @digit } {? . {+ @digit } } {? {| e | E } {? {| + | - } } {+ @digit } }
int ::= {? - } {+ @digit }
num ::= {+ @digit }
digit ::= 0 .. 9
Strings
Strings begin and end with ``"`` (double quote). Use ``""`` to represent
a double quote character within a string. In the grammar, strings are
identified with :production:`string`.
Keywords
The following character sequences are reserved keywords that cannot be
used as identifiers::
_ Axiom CoFixpoint Definition Fixpoint Hypothesis IF Parameter Prop
SProp Set Theorem Type Variable as at by cofix discriminated else
end exists exists2 fix for forall fun if in lazymatch let match
multimatch return then using where with
Note that plugins may define additional keywords when they are loaded.
Other tokens
The set of
tokens defined at any given time can vary because the :cmd:`Notation`
command can define new tokens. A :cmd:`Require` command may load more notation definitions,
while the end of a :cmd:`Section` may remove notations. Some notations
are defined in the basic library (see :ref:`thecoqlibrary`) and are normally
loaded automatically at startup time.
Here are the character sequences that Coq directly defines as tokens
without using :cmd:`Notation` (omitting 25 specialized tokens that begin with
``#int63_``)::
! #[ % & ' ( () (bfs) (dfs) ) * ** + , - ->
. .( .. ... / : ::= := :> :>> ; < <+ <- <:
<<: <= = => > >-> >= ? @ @{ [ [= ] _
`( `{ { {| | |- || }
When multiple tokens match the beginning of a sequence of characters,
the longest matching token is used.
Occasionally you may need to insert spaces to separate tokens. For example,
if ``~`` and ``~~`` are both defined as tokens, the inputs ``~ ~`` and
``~~`` generate different tokens, whereas if `~~` is not defined, then the
two inputs are equivalent.
.. _gallina-attributes:
Attributes
-----------
.. insertprodn all_attrs legacy_attr
.. prodn::
all_attrs ::= {* #[ {*, @attr } ] } {* @legacy_attr }
attr ::= @ident {? @attr_value }
attr_value ::= = @string
| ( {*, @attr } )
legacy_attr ::= {| Local | Global }
| {| Polymorphic | Monomorphic }
| {| Cumulative | NonCumulative }
| Private
| Program
Attributes modify the behavior of a command or tactic.
Syntactically, most commands and tactics can be decorated with attributes, but
attributes not supported by the command or tactic will be flagged as errors.
The order of top-level attributes doesn't affect their meaning. ``#[foo,bar]``, ``#[bar,foo]``,
``#[foo]#[bar]`` and ``#[bar]#[foo]`` are equivalent.
The legacy attributes (:n:`@legacy_attr`) provide an older, alternate syntax
for certain attributes. They are equivalent to new attributes as follows:
================ ================================
Legacy attribute New attribute
================ ================================
`Local` :attr:`local`
`Global` :attr:`global`
`Polymorphic` :attr:`universes(polymorphic)`
`Monomorphic` :attr:`universes(monomorphic)`
`Cumulative` :attr:`universes(cumulative)`
`NonCumulative` :attr:`universes(noncumulative)`
`Private` :attr:`private(matching)`
`Program` :attr:`program`
================ ================================
.. warn:: Unsupported attribute
This warning is an error by default. It is caused by using a
command with some attribute it does not understand.
|
