diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 200 |
5 files changed, 115 insertions, 110 deletions
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index c8fb4bd00e..789890eab5 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -285,19 +285,21 @@ Activating the Printing of Coercions Classes as Records ------------------ +.. index:: :> (coercion) + We allow the definition of *Structures with Inheritance* (or classes as records) by extending the existing :cmd:`Record` macro. Its new syntax is: .. cmdv:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } } - The first identifier `ident` is the name of the defined record and - `sort` is its type. The optional identifier after ``:=`` is the name - of the constuctor (it will be ``Build_``\ `ident` if not given). - The other identifiers are the names of the fields, and the `term` + The first identifier :token:`ident` is the name of the defined record and + :token:`sort` is its type. The optional identifier after ``:=`` is the name + of the constuctor (it will be :n:`Build_@ident` if not given). + The other identifiers are the names of the fields, and :token:`term` are their respective types. If ``:>`` is used instead of ``:`` in the declaration of a field, then the name of this field is automatically declared as a coercion from the record name to the class of this - field type. Remark that the fields always verify the uniform + field type. Note that the fields always verify the uniform inheritance condition. If the optional ``>`` is given before the record name, then the constructor name is automatically declared as a coercion from the class of the last field type to the record name diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index cc8870e2e4..e153c7cbe2 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -102,7 +102,7 @@ Syntactic control over equalities To give more control over the generation of equalities, the type checker will fall back directly to |Coq|’s usual typing of dependent -pattern matching if a return or in clause is specified. Likewise, the +pattern matching if a ``return`` or ``in`` clause is specified. Likewise, the if construct is not treated specially by |Program| so boolean tests in the code are not automatically reflected in the obligations. One can use the :g:`dec` combinator to get the correct hypotheses as in: @@ -118,8 +118,9 @@ use the :g:`dec` combinator to get the correct hypotheses as in: else S (pred n). The :g:`let` tupling construct :g:`let (x1, ..., xn) := t in b` does not -produce an equality, contrary to the let pattern construct :g:`let ’(x1, -..., xn) := t in b`. Also, :g:`term :>` explicitly asks the system to +produce an equality, contrary to the let pattern construct +:g:`let '(x1,..., xn) := t in b`. +Also, :g:`term :>` explicitly asks the system to coerce term to its support type. It can be useful in notations, for example: diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 882798205b..98dfcb2373 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -228,6 +228,8 @@ mechanism if available, as shown in the example. Substructures ~~~~~~~~~~~~~ +.. index:: :> (substructure) + Substructures are components of a class which are instances of a class themselves. They often arise when using classes for logical properties, e.g.: diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 85474a3e98..10650af1d1 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -97,8 +97,8 @@ Logic The basic library of |Coq| comes with the definitions of standard (intuitionistic) logical connectives (they are defined as inductive constructions). They are equipped with an appealing syntax enriching the -subclass `form` of the syntactic class `term`. The syntax of `form` -is shown below: +subclass :token:`form` of the syntactic class :token:`term`. The syntax of +:token:`form` is shown below: .. /!\ Please keep the blanks in the lines below, experimentally they produce a nice last column. Or even better, find a proper way to do this! diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 65df89da6c..1c53f5981d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1380,147 +1380,147 @@ Numeral notations .. cmd:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope. :name: Numeral Notation - This command allows the user to customize the way numeral literals - are parsed and printed. + This command allows the user to customize the way numeral literals + are parsed and printed. - The token :n:`@ident__1` should be the name of an inductive type, - while :n:`@ident__2` and :n:`@ident__3` should be the names of the - parsing and printing functions, respectively. The parsing function - :n:`@ident__2` should have one of the following types: + The token :n:`@ident__1` should be the name of an inductive type, + while :n:`@ident__2` and :n:`@ident__3` should be the names of the + parsing and printing functions, respectively. The parsing function + :n:`@ident__2` should have one of the following types: - * :n:`Decimal.int -> @ident__1` - * :n:`Decimal.int -> option @ident__1` - * :n:`Decimal.uint -> @ident__1` - * :n:`Decimal.uint -> option @ident__1` - * :n:`Z -> @ident__1` - * :n:`Z -> option @ident__1` + * :n:`Decimal.int -> @ident__1` + * :n:`Decimal.int -> option @ident__1` + * :n:`Decimal.uint -> @ident__1` + * :n:`Decimal.uint -> option @ident__1` + * :n:`Z -> @ident__1` + * :n:`Z -> option @ident__1` - And the printing function :n:`@ident__3` should have one of the - following types: + And the printing function :n:`@ident__3` should have one of the + following types: - * :n:`@ident__1 -> Decimal.int` - * :n:`@ident__1 -> option Decimal.int` - * :n:`@ident__1 -> Decimal.uint` - * :n:`@ident__1 -> option Decimal.uint` - * :n:`@ident__1 -> Z` - * :n:`@ident__1 -> option Z` + * :n:`@ident__1 -> Decimal.int` + * :n:`@ident__1 -> option Decimal.int` + * :n:`@ident__1 -> Decimal.uint` + * :n:`@ident__1 -> option Decimal.uint` + * :n:`@ident__1 -> Z` + * :n:`@ident__1 -> option Z` - When parsing, the application of the parsing function - :n:`@ident__2` to the number will be fully reduced, and universes - of the resulting term will be refreshed. + When parsing, the application of the parsing function + :n:`@ident__2` to the number will be fully reduced, and universes + of the resulting term will be refreshed. - .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). - When a literal larger than :token:`num` is parsed, a warning - message about possible stack overflow, resulting from evaluating - :n:`@ident__2`, will be displayed. + When a literal larger than :token:`num` is parsed, a warning + message about possible stack overflow, resulting from evaluating + :n:`@ident__2`, will be displayed. - .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (abstract after @num). + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (abstract after @num). - When a literal :g:`m` larger than :token:`num` is parsed, the - result will be :n:`(@ident__2 m)`, without reduction of this - application to a normal form. Here :g:`m` will be a - :g:`Decimal.int` or :g:`Decimal.uint` or :g:`Z`, depending on the - type of the parsing function :n:`@ident__2`. This allows for a - more compact representation of literals in types such as :g:`nat`, - and limits parse failures due to stack overflow. Note that a - warning will be emitted when an integer larger than :token:`num` - is parsed. Note that :n:`(abstract after @num)` has no effect - when :n:`@ident__2` lands in an :g:`option` type. + When a literal :g:`m` larger than :token:`num` is parsed, the + result will be :n:`(@ident__2 m)`, without reduction of this + application to a normal form. Here :g:`m` will be a + :g:`Decimal.int` or :g:`Decimal.uint` or :g:`Z`, depending on the + type of the parsing function :n:`@ident__2`. This allows for a + more compact representation of literals in types such as :g:`nat`, + and limits parse failures due to stack overflow. Note that a + warning will be emitted when an integer larger than :token:`num` + is parsed. Note that :n:`(abstract after @num)` has no effect + when :n:`@ident__2` lands in an :g:`option` type. - .. exn:: Cannot interpret this number as a value of type @type + .. exn:: Cannot interpret this number as a value of type @type - The numeral notation registered for :token:`type` does not support - the given numeral. This error is given when the interpretation - function returns :g:`None`, or if the interpretation is registered - for only non-negative integers, and the given numeral is negative. + The numeral notation registered for :token:`type` does not support + the given numeral. This error is given when the interpretation + function returns :g:`None`, or if the interpretation is registered + for only non-negative integers, and the given numeral is negative. - .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. + .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. - The parsing function given to the :cmd:`Numeral Notation` - vernacular is not of the right type. + The parsing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. - .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. + .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. - The printing function given to the :cmd:`Numeral Notation` - vernacular is not of the right type. + The printing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. - .. exn:: @type is not an inductive type. + .. exn:: @type is not an inductive type. - Numeral notations can only be declared for inductive types with no - arguments. + Numeral notations can only be declared for inductive types with no + arguments. - .. exn:: Unexpected term @term while parsing a numeral notation. + .. exn:: Unexpected term @term while parsing a numeral notation. - Parsing functions must always return ground terms, made up of - applications of constructors and inductive types. Parsing - functions may not return terms containing axioms, bare - (co)fixpoints, lambdas, etc. + Parsing functions must always return ground terms, made up of + applications of constructors and inductive types. Parsing + functions may not return terms containing axioms, bare + (co)fixpoints, lambdas, etc. - .. exn:: Unexpected non-option term @term while parsing a numeral notation. + .. exn:: Unexpected non-option term @term while parsing a numeral notation. - Parsing functions expected to return an :g:`option` must always - return a concrete :g:`Some` or :g:`None` when applied to a - concrete numeral expressed as a decimal. They may not return - opaque constants. + Parsing functions expected to return an :g:`option` must always + return a concrete :g:`Some` or :g:`None` when applied to a + concrete numeral expressed as a decimal. They may not return + opaque constants. - .. exn:: Cannot interpret in @scope because @ident could not be found in the current environment. + .. exn:: Cannot interpret in @scope because @ident could not be found in the current environment. - The inductive type used to register the numeral notation is no - longer available in the environment. Most likely, this is because - the numeral notation was declared inside a functor for an - inductive type inside the functor. This use case is not currently - supported. + The inductive type used to register the numeral notation is no + longer available in the environment. Most likely, this is because + the numeral notation was declared inside a functor for an + inductive type inside the functor. This use case is not currently + supported. - Alternatively, you might be trying to use a primitive token - notation from a plugin which forgot to specify which module you - must :g:`Require` for access to that notation. + Alternatively, you might be trying to use a primitive token + notation from a plugin which forgot to specify which module you + must :g:`Require` for access to that notation. - .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). + .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). - The type passed to :cmd:`Numeral Notation` must be a single - identifier. + The type passed to :cmd:`Numeral Notation` must be a single + identifier. - .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). + .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). - Both functions passed to :cmd:`Numeral Notation` must be single - identifiers. + Both functions passed to :cmd:`Numeral Notation` must be single + identifiers. - .. exn:: The reference @ident was not found in the current environment. + .. exn:: The reference @ident was not found in the current environment. - Identifiers passed to :cmd:`Numeral Notation` must exist in the - global environment. + Identifiers passed to :cmd:`Numeral Notation` must exist in the + global environment. - .. exn:: @ident is bound to a notation that does not denote a reference. + .. exn:: @ident is bound to a notation that does not denote a reference. - Identifiers passed to :cmd:`Numeral Notation` must be global - references, or notations which denote to single identifiers. + Identifiers passed to :cmd:`Numeral Notation` must be global + references, or notations which denote to single identifiers. - .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). + .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). - When a :cmd:`Numeral Notation` is registered in the current scope - with :n:`(warning after @num)`, this warning is emitted when - parsing a numeral greater than or equal to :token:`num`. + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(warning after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. - .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @ident__2. + .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @ident__2. - When a :cmd:`Numeral Notation` is registered in the current scope - with :n:`(abstract after @num)`, this warning is emitted when - parsing a numeral greater than or equal to :token:`num`. - Typically, this indicates that the fully computed representation - of numerals can be so large that non-tail-recursive OCaml - functions run out of stack space when trying to walk them. + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(abstract after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. + Typically, this indicates that the fully computed representation + of numerals can be so large that non-tail-recursive OCaml + functions run out of stack space when trying to walk them. - For example + For example - .. coqtop:: all + .. coqtop:: all - Check 90000. + Check 90000. - .. warn:: The 'abstract after' directive has no effect when the parsing function (@ident__2) targets an option type. + .. warn:: The 'abstract after' directive has no effect when the parsing function (@ident__2) targets an option type. - As noted above, the :n:`(abstract after @num)` directive has no - effect when :n:`@ident__2` lands in an :g:`option` type. + As noted above, the :n:`(abstract after @num)` directive has no + effect when :n:`@ident__2` lands in an :g:`option` type. .. _TacticNotation: |