diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-13 11:05:48 +0200 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2018-04-14 15:44:29 +0200 |
| commit | 3cc6a433d025996ea4a61969517d45ffbc9fd8a9 (patch) | |
| tree | 6846570d84758373da6bffa36b3bb8e285703aa4 /doc/sphinx/proof-engine/detailed-tactic-examples.rst | |
| parent | 14f44c0e23c413314adf23ed1059acc5cd1fef2f (diff) | |
[sphinx] Fix many warnings.
Including cross-reference TODOs.
I took down the number of warnings from 300 to 50.
Diffstat (limited to 'doc/sphinx/proof-engine/detailed-tactic-examples.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/detailed-tactic-examples.rst | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index 932f96788..fda20bff3 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -6,6 +6,8 @@ Detailed examples of tactics This chapter presents detailed examples of certain tactics, to illustrate their behavior. +.. _dependent-induction: + dependent induction ------------------- @@ -316,7 +318,7 @@ explicit proof terms: This concludes our example. -See also: The ``induction`` :ref:`TODO-9-induction`, ``case`` :ref:`TODO-9-induction` and ``inversion`` :ref:`TODO-8.14-inversion` tactics. +See also: The :tacn:`induction`, :tacn:`case`, and :tacn:`inversion` tactics. autorewrite @@ -403,6 +405,8 @@ Example 2: Mac Carthy function autorewrite with base1 using reflexivity || simpl. +.. _quote: + quote ----- @@ -544,8 +548,7 @@ Combining variables and constants ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ One can have both variables and constants in abstracts terms; for -example, this is the case for the ``ring`` tactic -:ref:`TODO-25-ringandfieldtacticfamilies`. Then one must provide to +example, this is the case for the :tacn:`ring` tactic. Then one must provide to ``quote`` a list of *constructors of constants*. For example, if the list is ``[O S]`` then closed natural numbers will be considered as constants and other terms as variables. @@ -606,7 +609,7 @@ don’t expect miracles from it! See also: comments of source file ``plugins/quote/quote.ml`` -See also: the ``ring`` tactic :ref:`TODO-25-ringandfieldtacticfamilies` +See also: the :tacn:`ring` tactic. Using the tactical language @@ -868,7 +871,7 @@ Deciding type isomorphisms A more tricky problem is to decide equalities between types and modulo isomorphisms. Here, we choose to use the isomorphisms of the simply typed λ-calculus with Cartesian product and unit type (see, for -example, [:ref:`TODO-45`]). The axioms of this λ-calculus are given below. +example, :cite:`TODO-45`). The axioms of this λ-calculus are given below. .. coqtop:: in reset |