diff options
Diffstat (limited to 'doc/sphinx/addendum/program.rst')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 24 |
1 files changed, 9 insertions, 15 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index d6895f5fe5..fad45995d2 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. this should be just "_program", but refs to it don't work .. _programs: @@ -45,7 +42,7 @@ be considered as an object of type :g:`{x : T | P}` for any well-formed will generate an obligation for every such coercion. In the other direction, Russell will automatically insert a projection. -Another distinction is the treatment of pattern-matching. Apart from +Another distinction is the treatment of pattern matching. Apart from the following differences, it is equivalent to the standard match operation (see :ref:`extendedpatternmatching`). @@ -84,15 +81,15 @@ operation (see :ref:`extendedpatternmatching`). There are options to control the generation of equalities and coercions. -.. opt:: Program Cases +.. flag:: Program Cases - This controls the special treatment of pattern-matching generating equalities + This controls the special treatment of pattern matching generating equalities and disequalities when using |Program| (it is on by default). All pattern-matches and let-patterns are handled using the standard algorithm of |Coq| (see :ref:`extendedpatternmatching`) when this option is deactivated. -.. opt:: Program Generalized Coercion +.. flag:: Program Generalized Coercion This controls the coercion of general inductive types when using |Program| (the option is on by default). Coercion of subset types and pairs is still @@ -105,7 +102,7 @@ Syntactic control over equalities To give more control over the generation of equalities, the type checker will fall back directly to |Coq|’s usual typing of dependent -pattern-matching if a return or in clause is specified. Likewise, the +pattern matching if a return or in clause is specified. Likewise, the if construct is not treated specially by |Program| so boolean tests in the code are not automatically reflected in the obligations. One can use the :g:`dec` combinator to get the correct hypotheses as in: @@ -213,7 +210,7 @@ with mutually recursive definitions too. end. Here we have one obligation for each branch (branches for :g:`0` and -``(S 0)`` are automatically generated by the pattern-matching +``(S 0)`` are automatically generated by the pattern matching compilation algorithm). .. coqtop:: all @@ -320,19 +317,19 @@ optional tactic is replaced by the default one if not specified. Shows the term that will be fed to the kernel once the obligations are solved. Useful for debugging. -.. opt:: Transparent Obligations +.. flag:: Transparent Obligations Controls whether all obligations should be declared as transparent (the default), or if the system should infer which obligations can be declared opaque. -.. opt:: Hide Obligations +.. flag:: Hide Obligations Controls whether obligations appearing in the term should be hidden as implicit arguments of the special constantProgram.Tactics.obligation. -.. opt:: Shrink Obligations +.. flag:: Shrink Obligations *Deprecated since 8.7* @@ -378,6 +375,3 @@ Frequently Asked Questions using lazy evaluation; #. Mutual recursion on the underlying inductive type isn’t possible anymore, but nested mutual recursion is always possible. - -.. bibliography:: ../biblio.bib - :keyprefix: p- |