aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/sphinx/README.rst3
-rw-r--r--doc/sphinx/addendum/miscellaneous-extensions.rst1
-rw-r--r--doc/sphinx/language/cic.rst18
-rw-r--r--doc/sphinx/language/coq-library.rst5
-rw-r--r--doc/sphinx/language/gallina-extensions.rst14
-rw-r--r--doc/sphinx/language/gallina-specification-language.rst6
-rw-r--r--doc/sphinx/practical-tools/utilities.rst4
-rw-r--r--doc/sphinx/proof-engine/detailed-tactic-examples.rst6
-rw-r--r--doc/sphinx/proof-engine/proof-handling.rst2
-rw-r--r--doc/sphinx/proof-engine/ssreflect-proof-language.rst1
-rw-r--r--doc/sphinx/proof-engine/tactics.rst19
-rw-r--r--doc/tools/coqrst/coqdomain.py8
12 files changed, 75 insertions, 12 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 32de15ee31..1643baf0e8 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -239,6 +239,9 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
http://docutils.sourceforge.net/docs/ref/rst/directives.html#generic-admonition
for more details.
+ Optionally, any text immediately following the ``.. example::`` header is
+ used as the example's title.
+
Example::
.. example:: Adding a hint to a database
diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst
index b6c35d8fa7..0f2d35d044 100644
--- a/doc/sphinx/addendum/miscellaneous-extensions.rst
+++ b/doc/sphinx/addendum/miscellaneous-extensions.rst
@@ -32,6 +32,7 @@ When the proof ends two constants are defined:
ends with ``Qed``, and transparent if the proof ends with ``Defined``.
.. example::
+
.. coqtop:: all
Require Coq.derive.Derive.
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 98e81ebc65..6e0c1e1b61 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -723,6 +723,7 @@ each :math:`T` in :math:`(t:T)∈Γ_I` can be written as: :math:`∀Γ_P,∀Γ_{
the sort of the inductive type t (not to be confused with :math:`\Sort` which is the set of sorts).
.. example::
+
The declaration for parameterized lists is:
.. math::
@@ -741,6 +742,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is
| cons : A -> list A -> list A.
.. example::
+
The declaration for a mutual inductive definition of tree and forest
is:
@@ -763,6 +765,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is
| consf : tree -> forest -> forest.
.. example::
+
The declaration for a mutual inductive definition of even and odd is:
.. math::
@@ -811,6 +814,7 @@ contains an inductive declaration.
E[Γ] ⊢ c : C
.. example::
+
Provided that our environment :math:`E` contains inductive definitions we showed before,
these two inference rules above enable us to conclude that:
@@ -919,6 +923,7 @@ condition* for a constant :math:`X` in the following cases:
.. example::
+
For instance, if one considers the following variant of a tree type
branching over the natural numbers:
@@ -985,6 +990,7 @@ the Type hierarchy.
.. example::
+
It is well known that the existential quantifier can be encoded as an
inductive definition. The following declaration introduces the second-
order existential quantifier :math:`∃ X.P(X)`.
@@ -1102,6 +1108,7 @@ sorts at each instance of a pattern-matching (see Section :ref:`Destructors`). A
an example, let us consider the following definition:
.. example::
+
.. coqtop:: in
Inductive option (A:Type) : Type :=
@@ -1118,6 +1125,7 @@ if :g:`option` is applied to a type in :math:`\Prop`, then, the result is not se
if set in :math:`\Prop`.
.. example::
+
.. coqtop:: all
Check (fun A:Set => option A).
@@ -1126,6 +1134,7 @@ if set in :math:`\Prop`.
Here is another example.
.. example::
+
.. coqtop:: in
Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B.
@@ -1136,6 +1145,7 @@ none in :math:`\Type`, and in :math:`\Type` otherwise. In all cases, the three k
eliminations schemes are allowed.
.. example::
+
.. coqtop:: all
Check (fun A:Set => prod A).
@@ -1324,6 +1334,7 @@ the extraction mechanism. Assume :math:`A` and :math:`B` are two propositions, a
logical disjunction :math:`A ∨ B` is defined inductively by:
.. example::
+
.. coqtop:: in
Inductive or (A B:Prop) : Prop :=
@@ -1334,6 +1345,7 @@ The following definition which computes a boolean value by case over
the proof of :g:`or A B` is not accepted:
.. example::
+
.. coqtop:: all
Fail Definition choice (A B: Prop) (x:or A B) :=
@@ -1357,6 +1369,7 @@ property which are provably different, contradicting the proof-
irrelevance property which is sometimes a useful axiom:
.. example::
+
.. coqtop:: all
Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y.
@@ -1390,6 +1403,7 @@ be used for rewriting not only in logical propositions but also in any
type.
.. example::
+
.. coqtop:: all
Print eq_rec.
@@ -1421,6 +1435,7 @@ We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math:
.. example::
+
The following term in concrete syntax::
match t as l return P' with
@@ -1485,6 +1500,7 @@ definition :math:`\ind{r}{Γ_I}{Γ_C}` with :math:`Γ_C = [c_1 :C_1 ;…;c_n :C_
.. example::
+
Below is a typing rule for the term shown in the previous example:
.. inference:: list example
@@ -1634,6 +1650,7 @@ The following definitions are correct, we enter them using the :cmd:`Fixpoint`
command and show the internal representation.
.. example::
+
.. coqtop:: all
Fixpoint plus (n m:nat) {struct n} : nat :=
@@ -1810,6 +1827,7 @@ option ``-impredicative-set``. For example, using the ordinary `coqtop`
command, the following is rejected,
.. example::
+
.. coqtop:: all
Fail Definition id: Set := forall X:Set,X->X.
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 52c56d2bd2..9de30e2190 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -848,6 +848,7 @@ Notation Interpretation Precedence Associativity
.. example::
+
.. coqtop:: all reset
Require Import ZArith.
@@ -887,6 +888,7 @@ Notation Interpretation
=============== ===================
.. example::
+
.. coqtop:: all reset
Require Import Reals.
@@ -906,6 +908,7 @@ tactics (see Chapter :ref:`tactics`), there are also:
Proves that two real integer constants are different.
.. example::
+
.. coqtop:: all reset
Require Import DiscrR.
@@ -919,6 +922,7 @@ tactics (see Chapter :ref:`tactics`), there are also:
Allows unfolding the ``Rabs`` constant and splits corresponding conjunctions.
.. example::
+
.. coqtop:: all reset
Require Import Reals.
@@ -933,6 +937,7 @@ tactics (see Chapter :ref:`tactics`), there are also:
corresponding to the condition on each operand of the product.
.. example::
+
.. coqtop:: all reset
Require Import Reals.
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 394b928ada..7dd0a6e383 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -70,7 +70,9 @@ generates a variant type definition with just one constructor:
To build an object of type :n:`@ident`, one should provide the constructor
:n:`@ident₀` with the appropriate number of terms filling the fields of the record.
-.. example:: Let us define the rational :math:`1/2`:
+.. example::
+
+ Let us define the rational :math:`1/2`:
.. coqtop:: in
@@ -1849,15 +1851,15 @@ are named as expected.
.. example:: (continued)
-.. coqtop:: all
+ .. coqtop:: all
- Arguments p [s t] _ [u] _: rename.
+ Arguments p [s t] _ [u] _: rename.
- Check (p r1 (u:=c)).
+ Check (p r1 (u:=c)).
- Check (p (s:=a) (t:=b) r1 (u:=c) r2).
+ Check (p (s:=a) (t:=b) r1 (u:=c) r2).
- Fail Arguments p [s t] _ [w] _ : assert.
+ Fail Arguments p [s t] _ [w] _ : assert.
.. _displaying-implicit-args:
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 8250b4b3d6..da5cd00d72 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -758,6 +758,7 @@ Simple inductive types
the case of annotated inductive types — cf. next section).
.. example::
+
The set of natural numbers is defined as:
.. coqtop:: all
@@ -976,6 +977,7 @@ Mutually defined inductive types
reason, the parameters must be strictly the same for each inductive types.
.. example::
+
The typical example of a mutual inductive data type is the one for trees and
forests. We assume given two types :g:`A` and :g:`B` as variables. It can
be declared the following way.
@@ -1048,6 +1050,7 @@ of the type.
For co-inductive types, the only elimination principle is case analysis.
.. example::
+
An example of a co-inductive type is the type of infinite sequences of
natural numbers, usually called streams.
@@ -1067,6 +1070,7 @@ Definition of co-inductive predicates and blocks of mutually
co-inductive definitions are also allowed.
.. example::
+
An example of a co-inductive predicate is the extensional equality on
streams:
@@ -1129,6 +1133,7 @@ constructions.
.. example::
+
One can define the addition function as :
.. coqtop:: all
@@ -1201,6 +1206,7 @@ constructions.
inductive types.
.. example::
+
The size of trees and forests can be defined the following way:
.. coqtop:: all
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index e15bcb8e2c..59bc2d22aa 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -218,6 +218,7 @@ file timing data:
On ``Mac OS``, this works best if you’ve installed ``gnu-time``.
.. example::
+
For example, the output of ``make TIMED=1`` may look like
this:
@@ -295,6 +296,7 @@ file timing data:
files which take effectively no time to compile.
.. example::
+
For example, the output table from
``make print-pretty-timed-diff`` may look like this:
@@ -318,6 +320,7 @@ line timing data:
line-by-line timing information.
.. example::
+
For example, running ``make all TIMING=1`` may result in a file like this:
::
@@ -345,6 +348,7 @@ line timing data:
This target requires python to build the table.
.. example::
+
For example, running ``print-pretty-single-time-diff`` might give a table like this:
::
diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index 78719c1ef1..225df8d54c 100644
--- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst
+++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
@@ -341,8 +341,7 @@ involves conditional rewritings and shows how to deal with them using
the optional tactic of the ``Hint Rewrite`` command.
-.. example::
- Ackermann function
+.. example:: Ackermann function
.. coqtop:: in reset
@@ -370,8 +369,7 @@ the optional tactic of the ``Hint Rewrite`` command.
autorewrite with base0 using try reflexivity.
-.. example::
- MacCarthy function
+.. example:: MacCarthy function
.. coqtop:: in reset
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 44376080c3..a9d0c16376 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -375,6 +375,7 @@ or focus the next one.
The following example script illustrates all these features:
.. example::
+
.. coqtop:: all
Goal (((True /\ True) /\ True) /\ True) /\ True.
@@ -511,6 +512,7 @@ Requesting information
:token:`ident`
.. example::
+
.. coqtop:: all
Show Match nat.
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 6fb73a030f..8a2fc3996a 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -4632,6 +4632,7 @@ bookkeeping steps.
.. example::
+
The following example use the ``~~`` prenex notation for boolean negation:
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index e6bc84365c..fdb04bf9a0 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -207,6 +207,7 @@ Applying theorems
useful to advanced users.
.. example::
+
.. coqtop:: reset all
Inductive Option : Set :=
@@ -366,6 +367,7 @@ Applying theorems
.. warn:: When @term contains more than one non dependent product the tactic lapply only takes into account the first product.
.. example::
+
Assume we have a transitive relation ``R`` on ``nat``:
.. coqtop:: reset in
@@ -837,6 +839,7 @@ quantified variables or hypotheses until the goal is not any more a
quantification or an implication.
.. example::
+
.. coqtop:: all
Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C.
@@ -958,6 +961,7 @@ quantification or an implication.
.. exn:: Cannot move @ident after @ident : it depends on @ident.
.. example::
+
.. coqtop:: all
Goal forall x :nat, x = 0 -> forall z y:nat, y=y-> 0=x.
@@ -1082,6 +1086,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged.
obtain atomic ones.
.. example::
+
.. coqtop:: all
Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C.
@@ -1252,6 +1257,7 @@ Controlling the proof flow
respect to some term.
.. example::
+
.. coqtop:: reset none
Goal forall x y:nat, 0 <= x + y + y.
@@ -1567,6 +1573,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
performs induction using this subterm.
.. example::
+
.. coqtop:: reset all
Lemma induction_test : forall n:nat, n = n -> n <= n.
@@ -1636,6 +1643,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
those are generalized as well in the statement to prove.
.. example::
+
.. coqtop:: reset all
Lemma comm x y : x + y = y + x.
@@ -1744,6 +1752,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
still get enough information in the proofs.
.. example::
+
.. coqtop:: reset all
Lemma le_minus : forall n:nat, n < 1 -> n = 0.
@@ -1809,6 +1818,7 @@ and an explanation of the underlying technique.
Note that this tactic is only available after a ``Require Import FunInd``.
.. example::
+
.. coqtop:: reset all
Require Import FunInd.
@@ -2856,6 +2866,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
+ A constant can be marked to be never unfolded by ``cbn`` or ``simpl``:
.. example::
+
.. coqtop:: all
Arguments minus n m : simpl never.
@@ -2868,6 +2879,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
``/`` symbol in the argument list of the :cmd:`Arguments` vernacular command.
.. example::
+
.. coqtop:: all
Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
@@ -2880,6 +2892,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
always unfolded.
.. example::
+
.. coqtop:: all
Definition volatile := fun x : nat => x.
@@ -2890,6 +2903,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
such arguments.
.. example::
+
.. coqtop:: all
Arguments minus !n !m.
@@ -3180,6 +3194,7 @@ where :tacn:`auto` uses simple :tacn:`apply`). As a consequence, :tacn:`eauto`
can solve such a goal:
.. example::
+
.. coqtop:: all
Hint Resolve ex_intro.
@@ -3748,6 +3763,7 @@ The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would
fail:
.. example::
+
.. coqtop:: reset all
Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x.
@@ -3904,6 +3920,7 @@ equality must contain all the quantified variables in order for congruence to
match against it.
.. example::
+
.. coqtop:: reset all
Theorem T (A:Type) (f:A -> A) (g: A -> A -> A) a b: a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a.
@@ -4315,6 +4332,7 @@ declare new field structures. All declared field structures can be
printed with the Print Fields command.
.. example::
+
.. coqtop:: reset all
Require Import Reals.
@@ -4426,6 +4444,7 @@ Simple tactic macros
A simple example has more value than a long explanation:
.. example::
+
.. coqtop:: reset all
Ltac Solve := simpl; intros; auto.
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index c9487abf03..e6b71a8293 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -571,6 +571,9 @@ class ExampleDirective(BaseAdmonition):
http://docutils.sourceforge.net/docs/ref/rst/directives.html#generic-admonition
for more details.
+ Optionally, any text immediately following the ``.. example::`` header is
+ used as the example's title.
+
Example::
.. example:: Adding a hint to a database
@@ -583,13 +586,14 @@ class ExampleDirective(BaseAdmonition):
"""
node_class = nodes.admonition
directive_name = "example"
+ optional_arguments = 1
def run(self):
# ‘BaseAdmonition’ checks whether ‘node_class’ is ‘nodes.admonition’,
# and uses arguments[0] as the title in that case (in other cases, the
# title is unset, and it is instead set in the HTML visitor).
- assert not self.arguments # Arguments have been parsed as content
- self.arguments = ['Example']
+ assert len(self.arguments) <= 1
+ self.arguments = [": ".join(['Example'] + self.arguments)]
self.options['classes'] = ['admonition', 'note']
return super().run()
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:06:17 +0000