diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -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 |
3 files changed, 13 insertions, 8 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.: |