diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 3dc8707a34..574b91664d 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -529,7 +529,7 @@ A detailed example: Euclidean division ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The file ``Euclid`` contains the proof of Euclidean division. -The natural numbers used here are unary, represented by the type``nat``, +The natural numbers used here are unary, represented by the type ``nat``, which is defined by two constructors ``O`` and ``S``. This module contains a theorem ``eucl_dev``, whose type is:: diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 2ea0861e47..73d9b93482 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -117,7 +117,7 @@ parameters is any term :math:`f \, t_1 \ldots t_n`. .. example:: Morphisms Continuing the previous example, let ``union: forall (A : Type), list A -> list A -> list A`` - perform the union of two sets by appending one list to the other. ``union` is a binary + perform the union of two sets by appending one list to the other. ``union`` is a binary morphism parametric over ``A`` that respects the relation instance ``(set_eq A)``. The latter condition is proved by showing: |