aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/proof-engine/detailed-tactic-examples.rst
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/proof-engine/detailed-tactic-examples.rst')
-rw-r--r--doc/sphinx/proof-engine/detailed-tactic-examples.rst17
1 files changed, 10 insertions, 7 deletions
diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index 932f96788..84810ddba 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
@@ -733,7 +736,7 @@ and this length is decremented for each rotation down to, but not
including, 1 because for a list of length ``n``, we can make exactly
``n−1`` rotations to generate at most ``n`` distinct lists. Here, it
must be noticed that we use the natural numbers of Coq for the
-rotation counter. On Figure :ref:`TODO-9.1-tactic-language`, we can
+rotation counter. In :ref:`ltac-syntax`, we can
see that it is possible to use usual natural numbers but they are only
used as arguments for primitive tactics and they cannot be handled, in
particular, we cannot make computations with them. So, a natural
@@ -830,7 +833,7 @@ The pattern matching on goals allows a complete and so a powerful
backtracking when returning tactic values. An interesting application
is the problem of deciding intuitionistic propositional logic.
Considering the contraction-free sequent calculi LJT* of Roy Dyckhoff
-:ref:`TODO-56-biblio`, it is quite natural to code such a tactic
+:cite:`Dyc92`, it is quite natural to code such a tactic
using the tactic language as shown on figures: :ref:`Deciding
intuitionistic propositions (1) <decidingintuitionistic1>` and
:ref:`Deciding intuitionistic propositions (2)
@@ -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:`RC95`). The axioms of this λ-calculus are given below.
.. coqtop:: in reset