diff options
| author | Maxime Dénès | 2018-12-07 13:59:35 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-16 18:45:35 +0200 |
| commit | f69b14496b0783c2281db482682540b2e419b967 (patch) | |
| tree | b73aea9761cb99d49c3e1e4b37460e89473ef431 | |
| parent | f5d41cecf9bbdef785b5370b8fdec7afa8563fc4 (diff) | |
Update and fix documentation of Program Fixpoint with measure
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 56f84d0ff0..b410833d25 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -194,14 +194,14 @@ Program Fixpoint The optional order annotation follows the grammar: .. productionlist:: orderannot - order : measure `term` (`term`)? | wf `term` `term` + order : measure `term` [ `term` ] | wf `term` `ident` - + :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 term + :g:`R` is a relation on :g:`X`. :g:`X` defaults to :g:`nat` and :g:`R` + to :g:`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 |