diff options
Diffstat (limited to 'doc/sphinx/addendum/program.rst')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index a2940881dd..1c3fdeb430 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -135,8 +135,7 @@ support types, avoiding uses of proof-irrelevance that would come up when reasoning with equality on the subset types themselves. The next two commands are similar to their standard counterparts -Definition (see Section :ref:`gallina_def`) and Fixpoint -(see Section :ref:`TODO-1.3.4-Fixpoint`) +:cmd:`Definition` and :cmd:`Fixpoint` in that they define constants. However, they may require the user to prove some goals to construct the final definitions. @@ -197,7 +196,7 @@ The optional order annotation follows the grammar: + :g:`wf R x` which is equivalent to :g:`measure x (R)`. The structural fixpoint operator behaves just like the one of |Coq| (see -Section :ref:`TODO-1.3.4-Fixpoint`), except it may also generate obligations. It works +:cmd:`Fixpoint`), except it may also generate obligations. It works with mutually recursive definitions too. .. coqtop:: reset none |