diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/LICENSE | 4 | ||||
| -rw-r--r-- | doc/README.md | 102 | ||||
| -rw-r--r-- | doc/sphinx/biblio.bib | 32 | ||||
| -rw-r--r-- | doc/sphinx/credits.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/index.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/introduction.rst | 52 | ||||
| -rw-r--r-- | doc/sphinx/language/cic.rst | 231 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 24 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 27 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 18 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 206 |
11 files changed, 429 insertions, 274 deletions
diff --git a/doc/LICENSE b/doc/LICENSE index c9f574afb..3789d9104 100644 --- a/doc/LICENSE +++ b/doc/LICENSE @@ -2,7 +2,7 @@ The Coq Reference Manual is a collective work from the Coq Development Team whose members are listed in the file CREDITS of the Coq source package. All related documents (the LaTeX and BibTeX sources, the embedded png files, and the PostScript, PDF and html outputs) are -copyright (c) INRIA 1999-2006, with the exception of the Ubuntu font +copyright (c) INRIA 1999-2018, with the exception of the Ubuntu font file UbuntuMono-B.ttf, which is Copyright 2010,2011 Canonical Ltd and licensed under the Ubuntu font license, version 1.0 @@ -18,7 +18,7 @@ The Coq Standard Library is a collective work from the Coq Development Team whose members are listed in the file CREDITS of the Coq source package. All related documents (the Coq vernacular source files and the PostScript, PDF and html outputs) are copyright (c) INRIA -1999-2006. The material connected to the Standard Library is +1999-2018. The material connected to the Standard Library is distributed under the terms of the Lesser General Public License version 2.1 or later. diff --git a/doc/README.md b/doc/README.md new file mode 100644 index 000000000..6c6e1f01f --- /dev/null +++ b/doc/README.md @@ -0,0 +1,102 @@ +The Coq documentation +===================== + +The Coq documentation includes + +- A Reference Manual +- A document presenting the Coq standard library + +The documentation of the latest released version is available on the Coq +web site at [coq.inria.fr/documentation](http://coq.inria.fr/documentation). + +Additionnally, you can view the documentation for the current master version at +<https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=documentation>. + +The reference manual is written is reStructuredText and compiled +using Sphinx. See [`sphinx/README.rst`](sphinx/README.rst) +to learn more about the format that is used. + +The documentation for the standard library is generated from +the `.v` source files using coqdoc. + +Dependencies +------------ + +### HTML documentation + +To produce the complete documentation in HTML, you will need Coq dependencies +listed in [`INSTALL`](../INSTALL). Additionally, the Sphinx-based +reference manual requires Python 3, and the following Python packages: + + sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex + +You can install them using `pip3 install` or using your distribution's package +manager. E.g. under recent Debian-based operating systems (Debian 10 "Buster", +Ubuntu 18.04, ...) you can use: + + apt install python3-sphinx python3-pexpect python3-sphinx-rtd-theme \ + python3-bs4 python3-sphinxcontrib.bibtex python3-pip + +Then, install the missing Python3 Antlr4 package: + + pip3 install antlr4-python3-runtime + +Nix users should get the correct development environment to build the +HTML documentation from Coq's [`default.nix`](../default.nix) (note this +doesn't include the LaTeX packages needed to build the full documentation). + +### Other formats + +To produce the documentation in PDF and PostScript formats, the following +additional tools are required: + + - latex (latex2e) + - pdflatex + - dvips + - makeindex + +Install them using your package manager. E.g. on Debian / Ubuntu: + + apt install texlive-latex-extra texlive-fonts-recommended + +Compilation +----------- + +To produce all documentation about Coq in all formats, just run: + + ./configure # (if you hadn't already) + make doc + + +Alternatively, you can use some specific targets: + +- `make doc-ps` + to produce all PostScript documents + +- `make doc-pdf` + to produce all PDF documents + +- `make doc-html` + to produce all HTML documents + +- `make sphinx` + to produce the HTML version of the reference manual + +- `make stdlib` + to produce all formats of the Coq standard library + + +Also note the `-with-doc yes` option of `./configure` to enable the +build of the documentation as part of the default make target. + + +Installation +------------ + +To install all produced documents, do: + + make install-doc + +This will install the documentation in `/usr/share/doc/coq` unless you +specify another value through the `-docdir` option of `./configure` or the +`DOCDIR` environment variable. diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index 3e988709c..3574bf675 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -3,6 +3,21 @@ @String{lnai = "Lecture Notes in Artificial Intelligence"} @String{SV = "{Sprin-ger-Verlag}"} +@InCollection{Asp00, + Title = {Proof General: A Generic Tool for Proof Development}, + Author = {Aspinall, David}, + Booktitle = {Tools and Algorithms for the Construction and + Analysis of Systems, {TACAS} 2000}, + Publisher = {Springer Berlin Heidelberg}, + Year = {2000}, + Editor = {Graf, Susanne and Schwartzbach, Michael}, + Pages = {38--43}, + Series = {Lecture Notes in Computer Science}, + Volume = {1785}, + Doi = {10.1007/3-540-46419-0_3}, + ISBN = {978-3-540-67282-1}, +} + @Book{Bar81, author = {H.P. Barendregt}, publisher = {North-Holland}, @@ -290,16 +305,13 @@ the Calculus of Inductive Constructions}}, year = {1995} } -@Misc{Pcoq, - author = {Lemme Team}, - title = {Pcoq a graphical user-interface for {Coq}}, - note = {\url{http://www-sop.inria.fr/lemme/pcoq/}} -} - -@Misc{ProofGeneral, - author = {David Aspinall}, - title = {Proof General}, - note = {\url{https://proofgeneral.github.io/}} +@InProceedings{Pit16, + Title = {Company-Coq: Taking Proof General one step closer to a real IDE}, + Author = {Pit-Claudel, Clément and Courtieu, Pierre}, + Booktitle = {CoqPL'16: The Second International Workshop on Coq for PL}, + Year = {2016}, + Month = jan, + Doi = {10.5281/zenodo.44331}, } @Book{RC95, diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index 2562dec46..5d9324a65 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -1393,7 +1393,7 @@ Version 8.8 is the third release of |Coq| developed on a time-based development cycle. Its development spanned 6 months from the release of |Coq| 8.7 and was based on a public roadmap. The development process was coordinated by Matthieu Sozeau. Maxime Dénès was in charge of the -release process. +release process. Théo Zimmermann is the maintainer of this release. Many power users helped to improve the design of the new features via the bug tracker, the pull request system, the |Coq| development mailing diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index f3ae49381..baf2e0d98 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -84,3 +84,8 @@ This material (the Coq Reference Manual) may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at http://www.opencontent.org/openpub). Options A and B are not elected. + +.. [#PG] Proof-General is available at https://proofgeneral.github.io/. + Optionally, you can enhance it with the minor mode + Company-Coq :cite:`Pit16` + (see https://github.com/cpitclaudel/company-coq). diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index bc72877b6..c7bc69db4 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -28,37 +28,35 @@ programs called *tactics*. All services of the |Coq| proof assistant are accessible by interpretation of a command language called *the vernacular*. -Coq has an interactive mode in which commands are interpreted as the +Coq has an interactive mode in which commands are interpreted as the user types them in from the keyboard and a compiled mode where commands are processed from a file. -- The interactive mode may be used as a debugging mode in which the - user can develop his theories and proofs step by step, backtracking - if needed and so on. The interactive mode is run with the `coqtop` - command from the operating system (which we shall assume to be some - variety of UNIX in the rest of this document). +- In interactive mode, users can develop their theories and proofs step by + step, and query the system for available theorems and definitions. The + interactive mode is generally run with the help of an IDE, such + as CoqIDE, documented in :ref:`coqintegrateddevelopmentenvironment`, + Emacs with Proof-General :cite:`Asp00` [#PG]_, + or jsCoq to run Coq in your browser (see https://github.com/ejgallego/jscoq). + The `coqtop` read-eval-print-loop can also be used directly, for debugging + purposes. - The compiled mode acts as a proof checker taking a file containing a whole development in order to ensure its correctness. Moreover, |Coq|’s compiler provides an output file containing a compact representation of its input. The compiled mode is run with the `coqc` - command from the operating system. + command. -These two modes are documented in Chapter :ref:`thecoqcommands`. - -Other modes of interaction with |Coq| are possible: through an emacs shell -window, an emacs generic user-interface for proof assistant (Proof -General :cite:`ProofGeneral`) or through a customized -interface (PCoq :cite:`Pcoq`). These facilities are not -documented here. There is also a |Coq| Integrated Development Environment -described in :ref:`coqintegrateddevelopmentenvironment`. +.. seealso:: :ref:`thecoqcommands`. How to read this book ===================== -This is a Reference Manual, not a User Manual, so it is not made for a -continuous reading. However, it has some structure that is explained -below. +This is a Reference Manual, so it is not made for a continuous reading. +We recommend using the various indexes to quickly locate the documentation +you are looking for. There is a global index, and a number of specific indexes +for tactics, vernacular commands, and error messages and warnings. +Nonetheless, the manual has some structure that is explained below. - The first part describes the specification language, |Gallina|. Chapters :ref:`gallinaspecificationlanguage` and :ref:`extensionsofgallina` describe the concrete @@ -68,7 +66,7 @@ below. of the formalism. Chapter :ref:`themodulesystem` describes the module system. -- The second part describes the proof engine. It is divided in five +- The second part describes the proof engine. It is divided in six chapters. Chapter :ref:`vernacularcommands` presents all commands (we call them *vernacular commands*) that are not directly related to interactive proving: requests to the environment, complete or partial @@ -79,24 +77,24 @@ below. *tactics*. The language to combine these tactics into complex proof strategies is given in Chapter :ref:`ltac`. Examples of tactics are described in Chapter :ref:`detailedexamplesoftactics`. + Finally, the |SSR| proof language is presented in + Chapter :ref:`thessreflectprooflanguage`. -- The third part describes how to extend the syntax of |Coq|. It - corresponds to the Chapter :ref:`syntaxextensionsandinterpretationscopes`. +- The third part describes how to extend the syntax of |Coq| in + Chapter :ref:`syntaxextensionsandinterpretationscopes` and how to define + new induction principles in Chapter :ref:`proofschemes`. - In the fourth part more practical tools are documented. First in Chapter :ref:`thecoqcommands`, the usage of `coqc` (batch mode) and `coqtop` (interactive mode) with their options is described. Then, in Chapter :ref:`utilities`, various utilities that come with the |Coq| distribution are presented. Finally, Chapter :ref:`coqintegrateddevelopmentenvironment` - describes the |Coq| integrated development environment. + describes CoqIDE. - The fifth part documents a number of advanced features, including coercions, canonical structures, typeclasses, program extraction, and specialized solvers and tactics. See the table of contents for a complete list. -At the end of the document, after the global index, the user can find -specific indexes for tactics, vernacular commands, and error messages. - List of additional documentation ================================ @@ -109,5 +107,5 @@ Installation The |Coq| standard library A commented version of sources of the |Coq| standard library - (including only the specifications, the proofs are removed) is given - in the additional document `Library.ps`. + (including only the specifications, the proofs are removed) is + available at https://coq.inria.fr/stdlib/. diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index f6bab0267..b01a4ef0f 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -721,67 +721,68 @@ called the *context of parameters*. Furthermore, we must have that each :math:`T` in :math:`(t:T)∈Γ_I` can be written as: :math:`∀Γ_P,∀Γ_{\mathit{Arr}(t)}, S` where :math:`Γ_{\mathit{Arr}(t)}` is called the *Arity* of the inductive type t and :math:`S` is called the sort of the inductive type t (not to be confused with :math:`\Sort` which is the set of sorts). -** Examples** The declaration for parameterized lists is: - -.. math:: - \ind{1}{[\List:\Set→\Set]}{\left[\begin{array}{rcl} - \Nil & : & \forall A:\Set,\List~A \\ - \cons & : & \forall A:\Set, A→ \List~A→ \List~A - \end{array} - \right]} - -which corresponds to the result of the |Coq| declaration: .. example:: - .. coqtop:: in - - Inductive list (A:Set) : Set := - | nil : list A - | cons : A -> list A -> list A. + The declaration for parameterized lists is: -The declaration for a mutual inductive definition of tree and forest -is: + .. math:: + \ind{1}{[\List:\Set→\Set]}{\left[\begin{array}{rcl} + \Nil & : & \forall A:\Set,\List~A \\ + \cons & : & \forall A:\Set, A→ \List~A→ \List~A + \end{array} + \right]} -.. math:: - \ind{~}{\left[\begin{array}{rcl}\tree&:&\Set\\\forest&:&\Set\end{array}\right]} - {\left[\begin{array}{rcl} - \node &:& \forest → \tree\\ - \emptyf &:& \forest\\ - \consf &:& \tree → \forest → \forest\\ - \end{array}\right]} + which corresponds to the result of the |Coq| declaration: -which corresponds to the result of the |Coq| declaration: + .. coqtop:: in + + Inductive list (A:Set) : Set := + | nil : list A + | cons : A -> list A -> list A. .. example:: - .. coqtop:: in + The declaration for a mutual inductive definition of tree and forest + is: - Inductive tree : Set := - | node : forest -> tree - with forest : Set := - | emptyf : forest - | consf : tree -> forest -> forest. + .. math:: + \ind{~}{\left[\begin{array}{rcl}\tree&:&\Set\\\forest&:&\Set\end{array}\right]} + {\left[\begin{array}{rcl} + \node &:& \forest → \tree\\ + \emptyf &:& \forest\\ + \consf &:& \tree → \forest → \forest\\ + \end{array}\right]} -The declaration for a mutual inductive definition of even and odd is: + which corresponds to the result of the |Coq| declaration: -.. math:: - \ind{1}{\left[\begin{array}{rcl}\even&:&\nat → \Prop \\ - \odd&:&\nat → \Prop \end{array}\right]} - {\left[\begin{array}{rcl} - \evenO &:& \even~0\\ - \evenS &:& \forall n, \odd~n -> \even~(\kw{S}~n)\\ - \oddS &:& \forall n, \even~n -> \odd~(\kw{S}~n) - \end{array}\right]} + .. coqtop:: in -which corresponds to the result of the |Coq| declaration: + Inductive tree : Set := + | node : forest -> tree + with forest : Set := + | emptyf : forest + | consf : tree -> forest -> forest. .. example:: - .. coqtop:: in + The declaration for a mutual inductive definition of even and odd is: + + .. math:: + \ind{1}{\left[\begin{array}{rcl}\even&:&\nat → \Prop \\ + \odd&:&\nat → \Prop \end{array}\right]} + {\left[\begin{array}{rcl} + \evenO &:& \even~0\\ + \evenS &:& \forall n, \odd~n -> \even~(\kw{S}~n)\\ + \oddS &:& \forall n, \even~n -> \odd~(\kw{S}~n) + \end{array}\right]} + + which corresponds to the result of the |Coq| declaration: - Inductive even : nat -> prop := - | even_O : even 0 - | even_S : forall n, odd n -> even (S n) - with odd : nat -> prop := - | odd_S : forall n, even n -> odd (S n). + .. coqtop:: in + + Inductive even : nat -> prop := + | even_O : even 0 + | even_S : forall n, odd n -> even (S n) + with odd : nat -> prop := + | odd_S : forall n, even n -> odd (S n). @@ -838,8 +839,8 @@ rules, we need a few definitions: Arity of a given sort +++++++++++++++++++++ -A type :math:`T` is an *arity of sort s* if it converts to the sort s or to a -product :math:`∀ x:T,U` with :math:`U` an arity of sort s. +A type :math:`T` is an *arity of sort* :math:`s` if it converts to the sort :math:`s` or to a +product :math:`∀ x:T,U` with :math:`U` an arity of sort :math:`s`. .. example:: @@ -850,7 +851,7 @@ product :math:`∀ x:T,U` with :math:`U` an arity of sort s. Arity +++++ A type :math:`T` is an *arity* if there is a :math:`s∈ \Sort` such that :math:`T` is an arity of -sort s. +sort :math:`s`. .. example:: @@ -921,29 +922,29 @@ condition* for a constant :math:`X` in the following cases: For instance, if one considers the following variant of a tree type branching over the natural numbers: - .. coqtop:: in + .. coqtop:: in - Inductive nattree (A:Type) : Type := - | leaf : nattree A - | node : A -> (nat -> nattree A) -> nattree A. - End TreeExample. - - Then every instantiated constructor of ``nattree A`` satisfies the nested positivity - condition for ``nattree``: + Inductive nattree (A:Type) : Type := + | leaf : nattree A + | node : A -> (nat -> nattree A) -> nattree A. + End TreeExample. + + Then every instantiated constructor of ``nattree A`` satisfies the nested positivity + condition for ``nattree``: - + Type ``nattree A`` of constructor ``leaf`` satisfies the positivity condition for - ``nattree`` because ``nattree`` does not appear in any (real) arguments of the - type of that constructor (primarily because ``nattree`` does not have any (real) - arguments) ... (bullet 1) + + Type ``nattree A`` of constructor ``leaf`` satisfies the positivity condition for + ``nattree`` because ``nattree`` does not appear in any (real) arguments of the + type of that constructor (primarily because ``nattree`` does not have any (real) + arguments) ... (bullet 1) - + Type ``A → (nat → nattree A) → nattree A`` of constructor ``node`` satisfies the - positivity condition for ``nattree`` because: + + Type ``A → (nat → nattree A) → nattree A`` of constructor ``node`` satisfies the + positivity condition for ``nattree`` because: - - ``nattree`` occurs only strictly positively in ``A`` ... (bullet 3) + - ``nattree`` occurs only strictly positively in ``A`` ... (bullet 3) - - ``nattree`` occurs only strictly positively in ``nat → nattree A`` ... (bullet 3 + 2) + - ``nattree`` occurs only strictly positively in ``nat → nattree A`` ... (bullet 3 + 2) - - ``nattree`` satisfies the positivity condition for ``nattree A`` ... (bullet 1) + - ``nattree`` satisfies the positivity condition for ``nattree A`` ... (bullet 1) .. _Correctness-rules: @@ -978,35 +979,33 @@ provided that the following side conditions hold: One can remark that there is a constraint between the sort of the arity of the inductive type and the sort of the type of its constructors which will always be satisfied for the impredicative -sortProp but may fail to define inductive definition on sort Set and +sort :math:`\Prop` but may fail to define inductive definition on sort :math:`\Set` and generate constraints between universes for inductive definitions in the Type hierarchy. -**Examples**. It is well known that the existential quantifier can be encoded as an -inductive definition. The following declaration introduces the second- -order existential quantifier :math:`∃ X.P(X)`. - .. example:: + It is well known that the existential quantifier can be encoded as an + inductive definition. The following declaration introduces the second- + order existential quantifier :math:`∃ X.P(X)`. + .. coqtop:: in - + Inductive exProp (P:Prop->Prop) : Prop := | exP_intro : forall X:Prop, P X -> exProp P. -The same definition on Set is not allowed and fails: + The same definition on :math:`\Set` is not allowed and fails: -.. example:: .. coqtop:: all Fail Inductive exSet (P:Set->Prop) : Set := exS_intro : forall X:Set, P X -> exSet P. -It is possible to declare the same inductive definition in the -universe Type. The exType inductive definition has type -:math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT_intro}` -has type :math:`\Type(k)` with :math:`k<j` and :math:`k≤ i`. + It is possible to declare the same inductive definition in the + universe :math:`\Type`. The :g:`exType` inductive definition has type + :math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT_intro}` + has type :math:`\Type(k)` with :math:`k<j` and :math:`k≤ i`. -.. example:: .. coqtop:: all Inductive exType (P:Type->Prop) : Type := @@ -1019,9 +1018,9 @@ has type :math:`\Type(k)` with :math:`k<j` and :math:`k≤ i`. Template polymorphism +++++++++++++++++++++ -Inductive types declared in Type are polymorphic over their arguments -in Type. If :math:`A` is an arity of some sort and s is a sort, we write :math:`A_{/s}` -for the arity obtained from :math:`A` by replacing its sort with s. +Inductive types declared in :math:`\Type` are polymorphic over their arguments +in :math:`\Type`. If :math:`A` is an arity of some sort and math:`s` is a sort, we write :math:`A_{/s}` +for the arity obtained from :math:`A` by replacing its sort with :math:`s`. Especially, if :math:`A` is well-typed in some global environment and local context, then :math:`A_{/s}` is typable by typability of all products in the Calculus of Inductive Constructions. The following typing rule is @@ -1382,7 +1381,7 @@ this type. [I:Prop|I→ s] A *singleton definition* has only one constructor and all the -arguments of this constructor have type Prop. In that case, there is a +arguments of this constructor have type :math:`\Prop`. In that case, there is a canonical way to interpret the informative extraction on an object in that type, such that the elimination on any sort :math:`s` is legal. Typical examples are the conjunction of non-informative propositions and the @@ -1421,45 +1420,45 @@ corresponding to the :math:`c:C` constructor. We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math:`c`. -**Example.** -The following term in concrete syntax:: +.. example:: + The following term in concrete syntax:: - match t as l return P' with - | nil _ => t1 - | cons _ hd tl => t2 - end + match t as l return P' with + | nil _ => t1 + | cons _ hd tl => t2 + end -can be represented in abstract syntax as + can be represented in abstract syntax as -.. math:: - \case(t,P,f 1 | f 2 ) + .. math:: + \case(t,P,f 1 | f 2 ) -where + where -.. math:: - \begin{eqnarray*} - P & = & \lambda~l~.~P^\prime\\ - f_1 & = & t_1\\ - f_2 & = & \lambda~(hd:\nat)~.~\lambda~(tl:\List~\nat)~.~t_2 - \end{eqnarray*} + .. math:: + \begin{eqnarray*} + P & = & \lambda~l~.~P^\prime\\ + f_1 & = & t_1\\ + f_2 & = & \lambda~(hd:\nat)~.~\lambda~(tl:\List~\nat)~.~t_2 + \end{eqnarray*} -According to the definition: + According to the definition: -.. math:: - \{(\kw{nil}~\nat)\}^P ≡ \{(\kw{nil}~\nat) : (\List~\nat)\}^P ≡ (P~(\kw{nil}~\nat)) + .. math:: + \{(\kw{nil}~\nat)\}^P ≡ \{(\kw{nil}~\nat) : (\List~\nat)\}^P ≡ (P~(\kw{nil}~\nat)) -.. math:: - - \begin{array}{rl} - \{(\kw{cons}~\nat)\}^P & ≡\{(\kw{cons}~\nat) : (\nat→\List~\nat→\List~\nat)\}^P \\ - & ≡∀ n:\nat, \{(\kw{cons}~\nat~n) : \List~\nat→\List~\nat)\}^P \\ - & ≡∀ n:\nat, ∀ l:\List~\nat, \{(\kw{cons}~\nat~n~l) : \List~\nat)\}^P \\ - & ≡∀ n:\nat, ∀ l:\List~\nat,(P~(\kw{cons}~\nat~n~l)). - \end{array} + .. math:: + + \begin{array}{rl} + \{(\kw{cons}~\nat)\}^P & ≡\{(\kw{cons}~\nat) : (\nat→\List~\nat→\List~\nat)\}^P \\ + & ≡∀ n:\nat, \{(\kw{cons}~\nat~n) : \List~\nat→\List~\nat)\}^P \\ + & ≡∀ n:\nat, ∀ l:\List~\nat, \{(\kw{cons}~\nat~n~l) : \List~\nat)\}^P \\ + & ≡∀ n:\nat, ∀ l:\List~\nat,(P~(\kw{cons}~\nat~n~l)). + \end{array} -Given some :math:`P` then :math:`\{(\kw{nil}~\nat)\}^P` represents the expected type of :math:`f_1` , -and :math:`\{(\kw{cons}~\nat)\}^P` represents the expected type of :math:`f_2`. + Given some :math:`P` then :math:`\{(\kw{nil}~\nat)\}^P` represents the expected type of :math:`f_1` , + and :math:`\{(\kw{cons}~\nat)\}^P` represents the expected type of :math:`f_2`. .. _Typing-rule: @@ -1819,7 +1818,7 @@ while it will type-check, if one uses instead the `coqtop` ``-impredicative-set`` option.. The major change in the theory concerns the rule for product formation -in the sort Set, which is extended to a domain in any sort: +in the sort :math:`\Set`, which is extended to a domain in any sort: .. inference:: ProdImp @@ -1832,11 +1831,11 @@ in the sort Set, which is extended to a domain in any sort: This extension has consequences on the inductive definitions which are allowed. In the impredicative system, one can build so-called *large inductive definitions* like the example of second-order existential -quantifier (exSet). +quantifier (:g:`exSet`). There should be restrictions on the eliminations which can be performed on such definitions. The eliminations rules in the -impredicative system for sort Set become: +impredicative system for sort :math:`\Set` become: diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index c21d8d4ec..509ac92f8 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -23,8 +23,9 @@ expressions. In this sense, the :cmd:`Record` construction allows defining .. _record_grammar: .. productionlist:: `sentence` - record : `record_keyword` `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. + record : `record_keyword` `record_body` with … with `record_body` record_keyword : Record | Inductive | CoInductive + record_body : `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. field : `ident` [ `binders` ] : `type` [ where `notation` ] : | `ident` [ `binders` ] [: `type` ] := `term` @@ -167,12 +168,13 @@ and the syntax `term.(@qualid` |term_1| |term_n| `)` to `@qualid` |term_1| `…` In each case, `term` is the object projected and the other arguments are the parameters of the inductive type. + .. note:: Records defined with the ``Record`` keyword are not allowed to be recursive (references to the record's name in the type of its field raises an error). To define recursive records, one can use the ``Inductive`` and ``CoInductive`` keywords, resulting in an inductive or co-inductive record. - A *caveat*, however, is that records cannot appear in mutually inductive - (or co-inductive) definitions. + Definition of mutal inductive or co-inductive records are also allowed, as long + as all of the types in the block are records. .. note:: Induction schemes are automatically generated for inductive records. Automatic generation of induction schemes for non-recursive records @@ -1347,7 +1349,7 @@ folder ``path/fOO/Bar`` maps to ``Lib.fOO.Bar``. Subdirectories corresponding to invalid |Coq| identifiers are skipped, and, by convention, subdirectories named ``CVS`` or ``_darcs`` are skipped too. -Thanks to this mechanism, .vo files are made available through the +Thanks to this mechanism, ``.vo`` files are made available through the logical name of the folder they are in, extended with their own basename. For example, the name associated to the file ``path/fOO/Bar/File.vo`` is ``Lib.fOO.Bar.File``. The same caveat applies for @@ -1358,17 +1360,17 @@ wrong loadpath afterwards. Some folders have a special status and are automatically put in the path. |Coq| commands associate automatically a logical path to files in the repository trees rooted at the directory from where the command is -launched, coqlib/user-contrib/, the directories listed in the -`$COQPATH`, `${XDG_DATA_HOME}/coq/` and `${XDG_DATA_DIRS}/coq/` -environment variables (see`http://standards.freedesktop.org/basedir- -spec/basedir-spec-latest.html`_) with the same physical-to-logical -translation and with an empty logical prefix. +launched, ``coqlib/user-contrib/``, the directories listed in the +``$COQPATH``, ``${XDG_DATA_HOME}/coq/`` and ``${XDG_DATA_DIRS}/coq/`` +environment variables (see `XDG base directory specification +<http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html>`_) +with the same physical-to-logical translation and with an empty logical prefix. The command line option ``-R`` is a variant of ``-Q`` which has the strictly same behavior regarding loadpaths, but which also makes the corresponding ``.vo`` files available through their short names in a way not unlike the ``Import`` command (see :ref:`here <import_qualid>`). For instance, ``-R`` `path` ``Lib`` -associates to the ``filepath/fOO/Bar/File.vo`` the logical name +associates to the file path `path`\ ``/path/fOO/Bar/File.vo`` the logical name ``Lib.fOO.Bar.File``, but allows this file to be accessed through the short names ``fOO.Bar.File,Bar.File`` and ``File``. If several files with identical base name are present in different subdirectories of a @@ -2226,7 +2228,7 @@ existential variable used in the same context as its context of definition is wr Check (fun x y => _) 0 1. Existential variables can be named by the user upon creation using -the syntax ``?``\ `ident`. This is useful when the existential +the syntax :n:`?[@ident]`. This is useful when the existential variable needs to be explicitly handled later in the script (e.g. with a named-goal selector, see :ref:`goal-selectors`). diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index c26ae2a93..e13625286 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -38,6 +38,7 @@ At the end, the notation “``[entry sep … sep entry]``” stands for a possibly empty sequence of expressions parsed by the “``entry``” entry, separated by the literal “``sep``”. +.. _lexical-conventions: Lexical conventions =================== @@ -905,6 +906,32 @@ Parametrized inductive types sort for the inductive definition and will produce a less convenient rule for case elimination. +.. opt:: Uniform Inductive Parameters + + When this option is set (it is off by default), + inductive definitions are abstracted over their parameters + before typechecking constructors, allowing to write: + + .. coqtop:: all undo + + Set Uniform Inductive Parameters. + Inductive list3 (A:Set) : Set := + | nil3 : list3 + | cons3 : A -> list3 -> list3. + + This behavior is essentially equivalent to starting a new section + and using :cmd:`Context` to give the uniform parameters, like so + (cf. :ref:`section-mechanism`): + + .. coqtop:: all undo + + Section list3. + Context (A:Set). + Inductive list3 : Set := + | nil3 : list3 + | cons3 : A -> list3 -> list3. + End list3. + .. seealso:: Section :ref:`inductive-definitions` and the :tacn:`induction` tactic. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index d0a0d568e..45667b099 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3422,18 +3422,24 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Adds each :n:`Hint Unfold @ident`. - .. cmdv:: Hint %( Transparent %| Opaque %) @qualid - :name: Hint ( Transparent | Opaque ) + .. cmdv:: Hint Transparent {+ @qualid} + Hint Opaque {+ @qualid} + :name: Hint Transparent; Hint Opaque - This adds a transparency hint to the database, making :n:`@qualid` a - transparent or opaque constant during resolution. This information is used + This adds transparency hints to the database, making :n:`@qualid` + transparent or opaque constants during resolution. This information is used during unification of the goal with any lemma in the database and inside the discrimination network to relax or constrain it in the case of discriminated databases. - .. cmdv:: Hint %( Transparent %| Opaque %) {+ @ident} + .. cmdv:: Hint Variables %( Transparent %| Opaque %) + Hint Constants %( Transparent %| Opaque %) + :name: Hint Variables; Hint Constants - Declares each :n:`@ident` as a transparent or opaque constant. + This sets the transparency flag used during unification of + hints in the database for all constants or all variables, + overwritting the existing settings of opacity. It is advised + to use this just after a :cmd:`Create HintDb` command. .. cmdv:: Hint Extern @num {? @pattern} => @tactic :name: Hint Extern diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 3b95a37ed..dcefa293b 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -10,15 +10,14 @@ parses and prints objects, i.e. the translations between the concrete and internal representations of terms and commands. The main commands to provide custom symbolic notations for terms are -``Notation`` and ``Infix``. They are described in section :ref:`Notations`. There is also a -variant of ``Notation`` which does not modify the parser. This provides with a -form of abbreviation and it is described in Section :ref:`Abbreviations`. It is +:cmd:`Notation` and :cmd:`Infix`; they will be described in the +:ref:`next section <Notations>`. There is also a +variant of :cmd:`Notation` which does not modify the parser; this provides a +form of :ref:`abbreviation <Abbreviations>`. It is sometimes expected that the same symbolic notation has different meanings in -different contexts. To achieve this form of overloading, |Coq| offers a notion -of interpretation scope. This is described in Section :ref:`Scopes`. - -The main command to provide custom notations for tactics is ``Tactic Notation``. -It is described in Section :ref:`TacticNotation`. +different contexts; to achieve this form of overloading, |Coq| offers a notion +of :ref:`interpretation scopes <Scopes>`. +The main command to provide custom notations for tactics is :cmd:`Tactic Notation`. .. coqtop:: none @@ -44,7 +43,7 @@ logical conjunction (and). Such a notation is declared by Notation "A /\ B" := (and A B). -The expression :g:`(and A B)` is the abbreviated term and the string ``"A /\ B"`` +The expression :g:`(and A B)` is the abbreviated term and the string :g:`"A /\ B"` (called a *notation*) tells how it is symbolically written. A notation is always surrounded by double quotes (except when the @@ -66,15 +65,15 @@ example. A notation binds a syntactic expression to a term. Unless the parser and pretty-printer of Coq already know how to deal with the syntactic -expression (see 12.1.7), explicit precedences and associativity rules -have to be given. +expression (see :ref:`ReservingNotations`), explicit precedences and +associativity rules have to be given. .. note:: The right-hand side of a notation is interpreted at the time the notation is - given. In particular, disambiguation of constants, implicit arguments (see - Section :ref:`ImplicitArguments`), coercions (see Section :ref:`Coercions`), - etc. are resolved at the time of the declaration of the notation. + given. In particular, disambiguation of constants, :ref:`implicit arguments + <ImplicitArguments>`, :ref:`coercions <Coercions>`, etc. are resolved at the + time of the declaration of the notation. Precedences and associativity ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -106,13 +105,13 @@ is 100, for example 85 for disjunction and 80 for conjunction [#and_or_levels]_. Similarly, an associativity is needed to decide whether :g:`True /\ False /\ False` defaults to :g:`True /\ (False /\ False)` (right associativity) or to :g:`(True /\ False) /\ False` (left associativity). We may even consider that the -expression is not well- formed and that parentheses are mandatory (this is a “no +expression is not well-formed and that parentheses are mandatory (this is a “no associativity”) [#no_associativity]_. We do not know of a special convention of the associativity of disjunction and conjunction, so let us apply for instance a right associativity (which is the choice of Coq). Precedence levels and associativity rules of notations have to be -given between parentheses in a list of modifiers that the ``Notation`` +given between parentheses in a list of modifiers that the :cmd:`Notation` command understands. Here is how the previous examples refine. .. coqtop:: in @@ -122,9 +121,10 @@ command understands. Here is how the previous examples refine. By default, a notation is considered non associative, but the precedence level is mandatory (except for special cases whose level is -canonical). The level is either a number or the phrase `next level` -whose meaning is obvious. The list of levels already assigned is on -Figure 3.1. +canonical). The level is either a number or the phrase ``next level`` +whose meaning is obvious. +Some :ref:`associativities are predefined <init-notations>` in the +``Notations`` module. .. TODO I don't find it obvious -- CPC @@ -162,7 +162,7 @@ One can also define notations for binders. In the last case though, there is a conflict with the notation for type casts. The notation for types casts, as shown by the command :cmd:`Print Grammar constr` is at level 100. To avoid ``x : A`` being parsed as a type cast, -it is necessary to put x at a level below 100, typically 99. Hence, a correct +it is necessary to put ``x`` at a level below 100, typically 99. Hence, a correct definition is the following: .. coqtop:: all @@ -176,7 +176,7 @@ Simple factorization rules ~~~~~~~~~~~~~~~~~~~~~~~~~~ Coq extensible parsing is performed by *Camlp5* which is essentially a LL1 -parser: it decides which notation to parse by looking tokens from left to right. +parser: it decides which notation to parse by looking at tokens from left to right. Hence, some care has to be taken not to hide already existing rules by new rules. Some simple left factorization work has to be done. Here is an example. @@ -186,11 +186,11 @@ rules. Some simple left factorization work has to be done. Here is an example. Notation "x < y < z" := (x < y /\ y < z) (at level 70). In order to factorize the left part of the rules, the subexpression -referred by y has to be at the same level in both rules. However the -default behavior puts y at the next level below 70 in the first rule -(no associativity is the default), and at the level 200 in the second -rule (level 200 is the default for inner expressions). To fix this, we -need to force the parsing level of y, as follows. +referred by ``y`` has to be at the same level in both rules. However the +default behavior puts ``y`` at the next level below 70 in the first rule +(``no associativity`` is the default), and at the level 200 in the second +rule (``level 200`` is the default for inner expressions). To fix this, we +need to force the parsing level of ``y``, as follows. .. coqtop:: all @@ -198,9 +198,9 @@ need to force the parsing level of y, as follows. Notation "x < y < z" := (x < y /\ y < z) (at level 70, y at next level). For the sake of factorization with Coq predefined rules, simple rules -have to be observed for notations starting with a symbol: e.g. rules -starting with “{” or “(” should be put at level 0. The list of Coq -predefined notations can be found in Chapter :ref:`thecoqlibrary`. +have to be observed for notations starting with a symbol, e.g., rules +starting with “\ ``{``\ ” or “\ ``(``\ ” should be put at level 0. The list +of Coq predefined notations can be found in the chapter on :ref:`thecoqlibrary`. .. cmd:: Print Grammar constr. @@ -215,7 +215,7 @@ predefined notations can be found in Chapter :ref:`thecoqlibrary`. Displaying symbolic notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The command ``Notation`` has an effect both on the Coq parser and on the +The command :cmd:`Notation` has an effect both on the Coq parser and on the Coq printer. For example: .. coqtop:: all @@ -301,7 +301,7 @@ at the time of use of the notation. .. note:: Sometimes, a notation is expected only for the parser. To do so, the option ``only parsing`` is allowed in the list of modifiers - of ``Notation``. Conversely, the ``only printing`` modifier can be + of :cmd:`Notation`. Conversely, the ``only printing`` modifier can be used to declare that a notation should only be used for printing and should not declare a parsing rule. In particular, such notations do not modify the parser. @@ -309,7 +309,7 @@ at the time of use of the notation. The Infix command ~~~~~~~~~~~~~~~~~~ -The ``Infix`` command is a shortening for declaring notations of infix +The :cmd:`Infix` command is a shortening for declaring notations of infix symbols. .. cmd:: Infix "@symbol" := @term ({+, @modifier}). @@ -324,6 +324,8 @@ symbols. Infix "/\" := and (at level 80, right associativity). +.. _ReservingNotations: + Reserving notations ~~~~~~~~~~~~~~~~~~~ @@ -341,7 +343,7 @@ state of Coq. Reserving a notation is also useful for simultaneously defining an inductive type or a recursive constant and a notation for it. -.. note:: The notations mentioned on Figure 3.1 are reserved. Hence +.. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence their precedence and associativity cannot be changed. Simultaneous definition of terms and notations @@ -391,7 +393,7 @@ Locating notations To know to which notations a given symbol belongs to, use the :cmd:`Locate` command. You can call it on any (composite) symbol surrounded by double quotes. To locate a particular notation, use a string where the variables of the -notation are replaced by “_” and where possible single quotes inserted around +notation are replaced by “``_``” and where possible single quotes inserted around identifiers or tokens starting with a single quote are dropped. .. coqtop:: all @@ -404,7 +406,7 @@ Notations and binders Notations can include binders. This section lists different ways to deal with binders. For further examples, see also -Section :ref:`RecursiveNotationsWithBinders`. +:ref:`RecursiveNotationsWithBinders`. Binders bound in the notation and parsed as identifiers +++++++++++++++++++++++++++++++++++++++++++++++++++++++ @@ -490,7 +492,7 @@ the following: This is so because the grammar also contains rules starting with :g:`{}` and followed by a term, such as the rule for the notation :g:`{ A } + { B }` for the -constant :g:`sumbool` (see Section :ref:`specification`). +constant :g:`sumbool` (see :ref:`specification`). Then, in the rule, ``x ident`` is replaced by ``x at level 99 as ident`` meaning that ``x`` is parsed as a term at level 99 (as done in the notation for @@ -545,7 +547,7 @@ the next command fails because p does not bind in the instance of n. Notation "[> a , .. , b <]" := (cons a .. (cons b nil) .., cons b .. (cons a nil) ..). -.. _RecursiveNotationsWithBinders: +.. _RecursiveNotations: Notations with recursive patterns ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -563,7 +565,7 @@ confused with the three-dots notation “``…``” used in this manual to denot a sequence of arbitrary size. On the left-hand side, the part “``x s .. s y``” of the notation parses -any number of time (but at least one time) a sequence of expressions +any number of times (but at least one time) a sequence of expressions separated by the sequence of tokens ``s`` (in the example, ``s`` is just “``;``”). The right-hand side must contain a subterm of the form either @@ -572,7 +574,7 @@ called the *iterator* of the recursive notation is an arbitrary expression with distinguished placeholders and where :math:`t` is called the *terminating expression* of the recursive notation. In the example, we choose the names :math:`x` and :math:`y` but in practice they can of course be chosen -arbitrarily. Not atht the placeholder :math:`[~]_I` has to occur only once but +arbitrarily. Note that the placeholder :math:`[~]_I` has to occur only once but :math:`[~]_E` can occur several times. Parsing the notation produces a list of expressions which are used to @@ -595,9 +597,10 @@ and the terminating expression is ``nil``. Here are other examples: (t at level 39). Notations with recursive patterns can be reserved like standard -notations, they can also be declared within interpretation scopes (see -section 12.2). +notations, they can also be declared within +:ref:`interpretation scopes <Scopes>`. +.. _RecursiveNotationsWithBinders: Notations with recursive patterns involving binders ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -611,7 +614,8 @@ is: (ex (fun x => .. (ex (fun y => p)) ..)) (at level 200, x binder, y binder, right associativity). -The principle is the same as in Section 12.1.12 except that in the iterator +The principle is the same as in :ref:`RecursiveNotations` +except that in the iterator :math:`φ([~]_E , [~]_I)`, the placeholder :math:`[~]_E` can also occur in position of the binding variable of a ``fun`` or a ``forall``. @@ -620,8 +624,8 @@ binders, ``x`` and ``y`` must be marked as ``binder`` in the list of modifiers of the notation. The binders of the parsed sequence are used to fill the occurrences of the first placeholder of the iterating pattern which is repeatedly nested as many times as the number of binders generated. If ever the -generalization operator ``'`` (see Section 2.7.19) is used in the binding list, -the added binders are taken into account too. +generalization operator ``'`` (see :ref:`implicit-generalization`) is +used in the binding list, the added binders are taken into account too. Binders parsing exist in two flavors. If ``x`` and ``y`` are marked as binder, then a sequence such as :g:`a b c : T` will be accepted and interpreted as @@ -678,7 +682,7 @@ position of :g:`x`: In addition to ``global``, one can restrict the syntax of a sub-expression by using the entry names ``ident`` or ``pattern`` -already seen in Section :ref:`NotationsWithBinders`, even when the +already seen in :ref:`NotationsWithBinders`, even when the corresponding expression is not used as a binder in the right-hand side. E.g.: @@ -690,10 +694,14 @@ side. E.g.: Summary ~~~~~~~ -**Syntax of notations** +.. _NotationSyntax: + +Syntax of notations ++++++++++++++++++++ The different syntactic variants of the command Notation are given on the -following figure. The optional :token:`scope` is described in the Section 12.2. +following figure. The optional :production:`scope` is described in +:ref:`Scopes`. .. productionlist:: coq notation : [Local] Notation `string` := `term` [`modifiers`] [: `scope`]. @@ -743,14 +751,15 @@ following figure. The optional :token:`scope` is described in the Section 12.2. given to some notation, say ``"{ y } & { z }"`` in fact applies to the underlying ``"{ x }"``\-free rule which is ``"y & z"``). -**Persistence of notations** +Persistence of notations +++++++++++++++++++++++++ Notations do not survive the end of sections. .. cmd:: Local Notation @notation Notations survive modules unless the command ``Local Notation`` is used instead - of ``Notation``. + of :cmd:`Notation`. .. _Scopes: @@ -762,13 +771,13 @@ interpretation. Interpretation scopes provide a weak, purely syntactical form of notations overloading: the same notation, for instance the infix symbol ``+`` can be used to denote distinct definitions of the additive operator. Depending on which interpretation -scopes is currently open, the interpretation is different. +scopes are currently open, the interpretation is different. Interpretation scopes can include an interpretation for numerals and strings. However, this is only made possible at the Objective Caml level. -See Figure 12.1 for the syntax of notations including the possibility -to declare them in a given scope. Here is a typical example which +See :ref:`above <NotationSyntax>` for the syntax of notations including the +possibility to declare them in a given scope. Here is a typical example which declares the notation for conjunction in the scope ``type_scope``. .. coqdoc:: @@ -892,27 +901,27 @@ Binding arguments of a constant to an interpretation scope turn to be themselves arguments of a reference are interpreted accordingly to the arguments scopes bound to this reference. -.. cmdv:: Arguments @qualid : clear scopes + .. cmdv:: Arguments @qualid : clear scopes - Arguments scopes can be cleared with :n:`Arguments @qualid : clear scopes`. + Arguments scopes can be cleared with :n:`Arguments @qualid : clear scopes`. -.. cmdv:: Arguments @qualid {+ @name%scope} : extra scopes + .. cmdv:: Arguments @qualid {+ @name%scope} : extra scopes - Defines extra argument scopes, to be used in case of coercion to Funclass - (see Chapter :ref:`implicitcoercions`) or with a computed type. + Defines extra argument scopes, to be used in case of coercion to ``Funclass`` + (see the :ref:`implicitcoercions` chapter) or with a computed type. -.. cmdv:: Global Arguments @qualid {+ @name%@scope} + .. cmdv:: Global Arguments @qualid {+ @name%@scope} - This behaves like :n:`Arguments qualid {+ @name%@scope}` but survives when a - section is closed instead of stopping working at section closing. Without the - ``Global`` modifier, the effect of the command stops when the section it belongs - to ends. + This behaves like :n:`Arguments qualid {+ @name%@scope}` but survives when a + section is closed instead of stopping working at section closing. Without the + ``Global`` modifier, the effect of the command stops when the section it belongs + to ends. -.. cmdv:: Local Arguments @qualid {+ @name%@scope} + .. cmdv:: Local Arguments @qualid {+ @name%@scope} - This behaves like :n:`Arguments @qualid {+ @name%@scope}` but does not - survive modules and files. Without the ``Local`` modifier, the effect of the - command is visible from within other modules or files. + This behaves like :n:`Arguments @qualid {+ @name%@scope}` but does not + survive modules and files. Without the ``Local`` modifier, the effect of the + command is visible from within other modules or files. .. seealso:: @@ -947,18 +956,18 @@ Binding types of arguments to an interpretation scope When an interpretation scope is naturally associated to a type (e.g. the scope of operations on the natural numbers), it may be convenient to bind it - to this type. When a scope ``scope`` is bound to a type type, any new function - defined later on gets its arguments of type type interpreted by default in + to this type. When a scope ``scope`` is bound to a type ``type``, any new function + defined later on gets its arguments of type ``type`` interpreted by default in scope scope (this default behavior can however be overwritten by explicitly - using the command ``Arguments``). + using the command :cmd:`Arguments`). Whether the argument of a function has some type ``type`` is determined - statically. For instance, if f is a polymorphic function of type :g:`forall - X:Type, X -> X` and type :g:`t` is bound to a scope ``scope``, then :g:`a` of - type :g:`t` in :g:`f t a` is not recognized as an argument to be interpreted - in scope ``scope``. + statically. For instance, if ``f`` is a polymorphic function of type + :g:`forall X:Type, X -> X` and type :g:`t` is bound to a scope ``scope``, + then :g:`a` of type :g:`t` in :g:`f t a` is not recognized as an argument to + be interpreted in scope ``scope``. - More generally, any coercion :n:`@class` (see Chapter :ref:`implicitcoercions`) + More generally, any coercion :n:`@class` (see the :ref:`implicitcoercions` chapter) can be bound to an interpretation scope. The command to do it is :n:`Bind Scope @scope with @class` @@ -980,12 +989,6 @@ Binding types of arguments to an interpretation scope .. note:: The scopes ``type_scope`` and ``function_scope`` also have a local effect on interpretation. See the next section. -.. seealso:: - - :cmd:`About` - The command to show the scopes bound to the arguments of a - function is described in Section 2. - The ``type_scope`` interpretation scope ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -996,7 +999,7 @@ scope which is temporarily activated each time a subterm of an expression is expected to be a type. It is delimited by the key ``type``, and bound to the coercion class ``Sortclass``. It is also used in certain situations where an expression is statically known to be a type, including the conclusion and the -type of hypotheses within an Ltac goal match (see Section +type of hypotheses within an Ltac goal match (see :ref:`ltac-match-goal`), the statement of a theorem, the type of a definition, the type of a binder, the domain and codomain of implication, the codomain of products, and more generally any type argument of a declared or defined @@ -1017,8 +1020,8 @@ Interpretation scopes used in the standard library of Coq ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We give an overview of the scopes used in the standard library of Coq. -For a complete list of notations in each scope, use the commands Print -Scopes or Print Scope scope. +For a complete list of notations in each scope, use the commands :cmd:`Print +Scopes` or :cmd:`Print Scope`. ``type_scope`` This scope includes infix * for product types and infix + for sum types. It @@ -1084,7 +1087,7 @@ Scopes or Print Scope scope. ``string_scope`` This scope includes notation for strings as elements of the type string. Special characters and escaping follow Coq conventions on strings (see - Section 1.1). Especially, there is no convention to visualize non + :ref:`lexical-conventions`). Especially, there is no convention to visualize non printable characters of a string. The file :file:`String.v` shows an example that contains quotes, a newline and a beep (i.e. the ASCII character of code 7). @@ -1093,8 +1096,8 @@ Scopes or Print Scope scope. This scope includes interpretation for all strings of the form ``"c"`` where :g:`c` is an ASCII character, or of the form ``"nnn"`` where nnn is a three-digits number (possibly with leading 0's), or of the form - ``""""``. Their respective denotations are the ASCII code of c, the - decimal ASCII code nnn, or the ascii code of the character ``"`` (i.e. + ``""""``. Their respective denotations are the ASCII code of :g:`c`, the + decimal ASCII code ``nnn``, or the ascii code of the character ``"`` (i.e. the ASCII code 34), all of them being represented in the type :g:`ascii`. @@ -1109,25 +1112,26 @@ Displaying informations about scopes by the same notation in a more recently open scope are not displayed. Hence each notation is displayed only once. -.. cmdv:: Print Visibility scope - - This displays the current stack of notations in scopes and lonely - notations assuming that scope is pushed on top of the stack. This is - useful to know how a subterm locally occurring in the scope ofscope is - interpreted. - -.. cmdv:: Print Scope scope + .. cmdv:: Print Visibility @scope - This displays all the notations defined in interpretation scopescope. - It also displays the delimiting key if any and the class to which the - scope is bound, if any. + This displays the current stack of notations in scopes and lonely + notations assuming that :token:`scope` is pushed on top of the stack. This is + useful to know how a subterm locally occurring in the scope :token:`scope` is + interpreted. -.. cmdv:: Print Scopes +.. cmd:: Print Scopes This displays all the notations, delimiting keys and corresponding class of all the existing interpretation scopes. It also displays the lonely notations. + .. cmdv:: Print Scope @scope + :name: Print Scope + + This displays all the notations defined in interpretation scope :token:`scope`. + It also displays the delimiting key if any and the class to which the + scope is bound, if any. + .. _Abbreviations: Abbreviations @@ -1324,7 +1328,7 @@ tactic language. Tactic notations obey the following syntax: .. [#and_or_levels] which are the levels effectively chosen in the current implementation of Coq -.. [#no_associativity] Coq accepts notations declared as no associative but the parser on +.. [#no_associativity] Coq accepts notations declared as ``no associative`` but the parser on which Coq is built, namely Camlp4, currently does not implement the - no-associativity and replaces it by a left associativity; hence it is - the same for Coq: no-associativity is in fact left associativity + ``no associativity`` and replaces it by a ``left associativity``; hence it is + the same for Coq: ``no associativity`` is in fact ``left associativity``. |