diff options
| author | Clément Pit-Claudel | 2018-11-25 19:31:18 -0500 |
|---|---|---|
| committer | Clément Pit-Claudel | 2018-11-25 19:31:18 -0500 |
| commit | b400fa987dec3c2dabfd69ce305d3ab8f1dc8952 (patch) | |
| tree | a1bf762b871f654a02d175dbb86b5e87c392fff0 /doc/sphinx/addendum/program.rst | |
| parent | e0f55aecee2ed9fc6f56979c255688e08b136c20 (diff) | |
| parent | e367f1113738b28c42de6c87b7c9f3d0fce3f5be (diff) | |
Merge PR #9036: Add bodies to sphinx objects.
Diffstat (limited to 'doc/sphinx/addendum/program.rst')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 25 |
1 files changed, 13 insertions, 12 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index fad45995d2..cc8870e2e4 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -150,6 +150,7 @@ Program Definition .. exn:: @ident already exists. :name: @ident already exists. (Program Definition) + :undocumented: .. cmdv:: Program Definition @ident : @type := @term @@ -162,7 +163,7 @@ Program Definition and the aforementioned coercion derivation are solved. .. exn:: In environment … the term: @term does not have type @type. Actually, it has type ... - + :undocumented: .. cmdv:: Program Definition @ident @binders : @type := @term @@ -181,21 +182,21 @@ Program Fixpoint .. cmd:: Program Fixpoint @ident @params {? {@order}} : @type := @term -The optional order annotation follows the grammar: + The optional order annotation follows the grammar: -.. productionlist:: orderannot - order : measure `term` (`term`)? | wf `term` `term` + .. productionlist:: orderannot + order : measure `term` (`term`)? | wf `term` `term` -+ :g:`measure f ( R )` where :g:`f` is a value of type :g:`X` computed on - any subset of the arguments and the optional (parenthesised) term - ``(R)`` is a relation on ``X``. By default ``X`` defaults to ``nat`` and ``R`` - to ``lt``. + + :g:`measure f ( R )` where :g:`f` is a value of type :g:`X` computed on + any subset of the arguments and the optional (parenthesised) term + ``(R)`` is a relation on ``X``. By default ``X`` defaults to ``nat`` and ``R`` + to ``lt``. -+ :g:`wf R x` which is equivalent to :g:`measure x (R)`. + + :g:`wf R x` which is equivalent to :g:`measure x (R)`. -The structural fixpoint operator behaves just like the one of |Coq| (see -:cmd:`Fixpoint`), except it may also generate obligations. It works -with mutually recursive definitions too. + The structural fixpoint operator behaves just like the one of |Coq| (see + :cmd:`Fixpoint`), except it may also generate obligations. It works + with mutually recursive definitions too. .. coqtop:: reset in |