diff options
| author | Théo Zimmermann | 2019-11-14 13:09:27 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-11-14 13:09:27 +0100 |
| commit | bfa987e3acd02b9cc10951b147ce229d17768ab9 (patch) | |
| tree | 80d93a31d9e79672dd1e98283dfc955afe931819 /doc/sphinx/addendum | |
| parent | b9def53df5a69d5d4dbf46bd846281220b4fe1db (diff) | |
| parent | 78ed4a1df20ef71ee3ed94c1c8c9d490001ac328 (diff) | |
Merge PR #11100: small documentation fixes
Reviewed-by: Zimmi48
Ack-by: cpitclaudel
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 9f92fc4c56..0754145b39 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -530,7 +530,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 93a1be027c..4feda5e875 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: |