diff options
| author | Hugo Herbelin | 2020-05-06 16:59:19 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-06 23:09:33 +0200 |
| commit | 037c8d299ca1a5aef9813133dca07ad6f35e1e75 (patch) | |
| tree | 0aed06d378c8b5291621685fd542d742a9224af2 /doc/sphinx/language/core/basic.rst | |
| parent | 20f0e2efb87541e511cf31e220a44e4376c44550 (diff) | |
Keywords: Applying suggestions from Jim Fehrle and Théo Zimmermann.
Diffstat (limited to 'doc/sphinx/language/core/basic.rst')
| -rw-r--r-- | doc/sphinx/language/core/basic.rst | 31 |
1 files changed, 19 insertions, 12 deletions
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 3940242bb3..aa93b4d21f 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -130,31 +130,38 @@ Strings identified with :production:`string`. Keywords - The following character sequences are reserved keywords that cannot be - used as identifiers:: + The following character sequences are keywords defined in the main Coq grammar + that cannot be used as identifiers (even when starting Coq with the `-noinit` + command-line flag):: _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop SProp Set Theorem Type Variable as at cofix else end fix for forall fun if in let match return then where with - Note that notations and plugins may define additional keywords. + The following are keywords defined in notations or plugins loaded in the :term:`prelude`:: -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 standard library (see :ref:`thecoqlibrary`) and are generally - loaded automatically at startup time. + IF by exists exists2 using + + Note that loading additional modules or plugins may expand the set of reserved + keywords. - Here are the character sequences that |Coq| directly defines as tokens - without using :cmd:`Notation`:: +Other tokens + The following character sequences are tokens defined in the main Coq grammar + (even when starting Coq with the `-noinit` command-line flag):: ! #[ % & ' ( () ) * + , - -> . .( .. ... / : ::= := :> :>> ; < <+ <- <: <<: <= = => > >-> >= ? @ @{ [ ] _ `( `{ { {| | } + The following character sequences are tokens defined in notations or plugins + loaded in the :term:`prelude`:: + + ** [= |- || -> + + Note that loading additional modules or plugins may expand the set of defined + tokens. + 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, |