diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/language/cic.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 35 |
2 files changed, 36 insertions, 1 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 67683902cd..962d2a94e3 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -51,7 +51,7 @@ function types over these data types. Consequently they also have a type. Because assuming simply that :math:`\Set` has type :math:`\Set` leads to an inconsistent theory :cite:`Coq86`, the language of |Cic| has infinitely many sorts. There are, in addition to :math:`\Set` and :math:`\Prop` -a hierarchy of universes :math:`\Type(i)` for any integer :math:`i`. +a hierarchy of universes :math:`\Type(i)` for any integer :math:`i ≥ 1`. Like :math:`\Set`, all of the sorts :math:`\Type(i)` contain small sets such as booleans, natural numbers, as well as products, subsets and function diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 590d71b5f3..24645a8cc3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -346,11 +346,46 @@ Navigation in the proof tree Goals are just existential variables and existential variables do not get a name by default. You can give a name to a goal by using :n:`refine ?[@ident]`. + You may also wrap this in an Ltac-definition like: + + .. coqtop:: in + + Ltac name_goal name := refine ?[name]. .. seealso:: :ref:`existential-variables` .. example:: + This first example uses the Ltac definition above, and the named goals + only serve for documentation. + + .. coqtop:: all + + Goal forall n, n + 0 = n. + Proof. + induction n; [ name_goal base | name_goal step ]. + [base]: { + + .. coqtop:: all + + reflexivity. + + .. coqtop:: in + + } + + .. coqtop:: all + + [step]: { + + .. coqtop:: all + + simpl. + f_equal. + assumption. + } + Qed. + This can also be a way of focusing on a shelved goal, for instance: .. coqtop:: all |