diff options
Diffstat (limited to 'doc/sphinx/language/core')
| -rw-r--r-- | doc/sphinx/language/core/assumptions.rst | 16 | ||||
| -rw-r--r-- | doc/sphinx/language/core/basic.rst | 47 | ||||
| -rw-r--r-- | doc/sphinx/language/core/definitions.rst | 16 | ||||
| -rw-r--r-- | doc/sphinx/language/core/sorts.rst | 24 | ||||
| -rw-r--r-- | doc/sphinx/language/core/variants.rst | 2 |
5 files changed, 53 insertions, 52 deletions
diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index 9943e0aa76..955f48b772 100644 --- a/doc/sphinx/language/core/assumptions.rst +++ b/doc/sphinx/language/core/assumptions.rst @@ -44,10 +44,11 @@ fun and forall gets identical. Moreover, parentheses can be omitted in the case of a single sequence of bindings sharing the same type (e.g.: :g:`fun (x y z : A) => t` can be shortened in :g:`fun x y z : A => t`). -.. index:: fun ... => ... +.. index:: fun +.. index:: forall -Abstractions: fun ------------------ +Functions (fun) and function types (forall) +------------------------------------------- .. insertprodn term_forall_or_fun term_forall_or_fun @@ -69,11 +70,6 @@ a let-binder occurs in the list of binders, it is expanded to a let-in definition (see Section :ref:`let-in`). -.. index:: forall - -Products: forall ----------------- - The expression :n:`forall @ident : @type, @term` denotes the *product* of the variable :n:`@ident` of type :n:`@type`, over the term :n:`@term`. As for abstractions, :g:`forall` is followed by a binder list, and products @@ -92,8 +88,8 @@ Non dependent product types have a special notation: :g:`A -> B` stands for :g:`forall _ : A, B`. The *non dependent product* is used both to denote the propositional implication and function types. -Applications ------------- +Function application +-------------------- .. insertprodn term_application arg diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 68900aa0be..64b29c1c0b 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -15,6 +15,8 @@ settings that |Coq| provides. Syntax and lexical conventions ------------------------------ +.. _syntax-conventions: + Syntax conventions ~~~~~~~~~~~~~~~~~~ @@ -55,7 +57,7 @@ appending the level to the nonterminal name (as in :n:`@term100` or |Coq| uses an extensible parser. Plugins and the :ref:`notation system <syntax-extensions-and-notation-scopes>` can extend the - syntax at run time. Some notations are defined in the prelude, + syntax at run time. Some notations are defined in the :term:`prelude`, which is loaded by default. The documented grammar doesn't include these notations. Precedence levels not used by the base grammar are omitted from the documentation, even though they could still be @@ -117,21 +119,19 @@ Numerals integer. Underscores embedded in the digits are ignored, for example ``1_000_000`` is the same as ``1000000``. - .. insertprodn numeral digit + .. insertprodn numeral hexdigit .. prodn:: - digit ::= 0 .. 9 - digitu ::= {| @digit | _ } - hexdigit ::= {| 0 .. 9 | a..f | A..F } - hexdigitu ::= {| @hexdigit | _ } - decnum ::= @digit {* @digitu } - hexnum ::= {| 0x | 0X } @hexdigit {* @hexdigitu } - num ::= {| @decnum | @hexnum } - sign ::= {| + | - } + numeral ::= {? - } @decnum {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnum } + | {? - } @hexnum {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnum } int ::= {? - } @num - decimal ::= @decnum {? . {+ @digitu } } {? {| e | E } {? @sign } @decnum } - hexadecimal ::= @hexnum {? . {+ @hexdigitu } } {? {| p | P } {? @sign } @decnum } - numeral ::= {? - } {| @decimal | @hexadecimal } + num ::= {| @decnum | @hexnum } + decnum ::= @digit {* {| @digit | _ } } + digit ::= 0 .. 9 + hexnum ::= {| 0x | 0X } @hexdigit {* {| @hexdigit | _ } } + hexdigit ::= {| 0 .. 9 | a .. f | A .. F } + + .. todo PR need some code fixes for hex, see PR 11948 Strings Strings begin and end with ``"`` (double quote). Use ``""`` to represent @@ -292,7 +292,7 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types document ::= {* @sentence } sentence ::= {? @attributes } @command . | {? @attributes } {? @num : } @query_command . - | {? @attributes } {? @toplevel_selector } @ltac_expr {| . | ... } + | {? @attributes } {? @toplevel_selector : } @ltac_expr {| . | ... } | @control_command :n:`@ltac_expr` syntax supports both simple and compound @@ -417,8 +417,16 @@ more precise description of the scope of these settings): .. FIXME Convert "Extraction Language" to an option. -Flags, options and tables are identified by a series of identifiers, each with an initial -capital letter. +.. insertprodn setting_name setting_name + +.. prodn:: + setting_name ::= {+ @ident } + +.. + + Flags, options and tables are identified by a series of + identifiers. By convention, each of the identifiers start with an + initial capital letter. Flags, options and tables appear in the HTML documentation in blue or gray boxes after the labels "Flag", "Option" and "Table". In the pdf, @@ -428,11 +436,6 @@ they appear after a boldface label. They are listed in the .. cmd:: Set @setting_name {? {| @int | @string } } :name: Set - .. insertprodn setting_name setting_name - - .. prodn:: - setting_name ::= {+ @ident } - If :n:`@setting_name` is a flag, no value may be provided; the flag is set to on. If :n:`@setting_name` is an option, a value of the appropriate type @@ -533,4 +536,4 @@ Newly opened modules and sections inherit the current settings. :cmd:`Unset` commands. If your goal is to define project-wide settings, you should rather use the command-line arguments ``-set`` and ``-unset`` for setting flags and options - (cf. :ref:`command-line-options`). + (see :ref:`command-line-options`). diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 0e637e5aa3..42203d9d65 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -34,18 +34,18 @@ Type cast .. insertprodn term_cast term_cast .. prodn:: - term_cast ::= @term10 <: @term - | @term10 <<: @term - | @term10 : @term + term_cast ::= @term10 <: @type + | @term10 <<: @type + | @term10 : @type | @term10 :> -The expression :n:`@term : @type` is a type cast expression. It enforces -the type of :n:`@term` to be :n:`@type`. +The expression :n:`@term10 : @type` is a type cast expression. It enforces +the type of :n:`@term10` to be :n:`@type`. -:n:`@term <: @type` locally sets up the virtual machine for checking that -:n:`@term` has type :n:`@type`. +:n:`@term10 <: @type` locally sets up the virtual machine for checking that +:n:`@term10` has type :n:`@type`. -:n:`@term <<: @type` uses native compilation for checking that :n:`@term` +:n:`@term10 <<: @type` uses native compilation for checking that :n:`@term10` has type :n:`@type`. .. _gallina-definitions: diff --git a/doc/sphinx/language/core/sorts.rst b/doc/sphinx/language/core/sorts.rst index 03581b95dd..3517d70005 100644 --- a/doc/sphinx/language/core/sorts.rst +++ b/doc/sphinx/language/core/sorts.rst @@ -30,14 +30,16 @@ and :math:`\Set`. The sort :math:`\Prop` intends to be the type of logical propositions. If :math:`M` is a logical proposition then it denotes the class of terms representing -proofs of :math:`M`. An object :math:`m` belonging to :math:`M` witnesses the fact that :math:`M` is -provable. An object of type :math:`\Prop` is called a proposition. +proofs of :math:`M`. An object :math:`m` belonging to :math:`M` +:term:`witnesses <witness>` the fact that :math:`M` is +provable. An object of type :math:`\Prop` is called a :gdef:`proposition`. We denote propositions by :n:`@form`. This constitutes a semantic subclass of the syntactic class :n:`@term`. The sort :math:`\SProp` is like :math:`\Prop` but the propositions in :math:`\SProp` are known to have irrelevant proofs (all proofs are -equal). Objects of type :math:`\SProp` are called strict propositions. +equal). Objects of type :math:`\SProp` are called +:gdef:`strict propositions <strict proposition>`. See :ref:`sprop` for information about using :math:`\SProp`, and :cite:`Gilbert:POPL2019` for meta theoretical considerations. @@ -66,12 +68,12 @@ Formally, we call :math:`\Sort` the set of sorts which is defined by: \Sort \equiv \{\SProp,\Prop,\Set,\Type(i)\;|\; i~∈ ℕ\} -Their properties, such as: :math:`\Prop:\Type(1)`, :math:`\Set:\Type(1)`, and -:math:`\Type(i):\Type(i+1)`, are defined in Section :ref:`subtyping-rules`. +Their properties, such as :math:`\Prop:\Type(1)`, :math:`\Set:\Type(1)`, and +:math:`\Type(i):\Type(i+1)`, are described in :ref:`subtyping-rules`. The user does not have to mention explicitly the index :math:`i` when -referring to the universe :math:`\Type(i)`. One only writes :math:`\Type`. The system -itself generates for each instance of :math:`\Type` a new index for the +referring to the universe :math:`\Type(i)`. One only writes `Type`. The system +itself generates for each instance of `Type` a new index for the universe and checks that the constraints between these indexes can be solved. From the user point of view we consequently have :math:`\Type:\Type`. We shall make precise in the typing rules the constraints between the @@ -81,8 +83,8 @@ indices. .. _Implementation-issues: **Implementation issues** In practice, the Type hierarchy is -implemented using *algebraic -universes*. An algebraic universe :math:`u` is either a variable (a qualified +implemented using algebraic universes. +An :gdef:`algebraic universe` :math:`u` is either a variable (a qualified identifier with a number) or a successor of an algebraic universe (an expression :math:`u+1`), or an upper bound of algebraic universes (an expression :math:`\max(u_1 ,...,u_n )`), or the base universe (the expression @@ -94,6 +96,6 @@ constraints between the universe variables is maintained globally. To ensure the existence of a mapping of the universes to the positive integers, the graph of constraints must remain acyclic. Typing expressions that violate the acyclicity of the graph of constraints -results in a Universe inconsistency error. +results in a :exn:`Universe inconsistency` error. -.. seealso:: :ref:`printing-universes`. +.. seealso:: :ref:`printing-universes`, :ref:`explicit-universes`. diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst index 6d4676b3c4..d00a2f4100 100644 --- a/doc/sphinx/language/core/variants.rst +++ b/doc/sphinx/language/core/variants.rst @@ -52,7 +52,7 @@ Private (matching) inductive types .. index:: match ... with ... -.. _match: +.. _match_term: Definition by cases: match -------------------------- |