diff options
Diffstat (limited to 'doc/sphinx/addendum/program.rst')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index cc8870e2e4..56f84d0ff0 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -95,6 +95,14 @@ coercions. (the option is on by default). Coercion of subset types and pairs is still active in this case. +.. flag:: Program Mode + + Enables the program mode, in which 1) typechecking allows subset coercions and + 2) the elaboration of pattern matching of :cmd:`Program Fixpoint` and + :cmd:`Program Definition` act + like Program Fixpoint/Definition, generating obligations if there are + unresolved holes after typechecking. + .. _syntactic_control: Syntactic control over equalities @@ -102,7 +110,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: @@ -118,8 +126,9 @@ use the :g:`dec` combinator to get the correct hypotheses as in: else S (pred n). The :g:`let` tupling construct :g:`let (x1, ..., xn) := t in b` does not -produce an equality, contrary to the let pattern construct :g:`let ’(x1, -..., xn) := t in b`. Also, :g:`term :>` explicitly asks the system to +produce an equality, contrary to the let pattern construct +:g:`let '(x1,..., xn) := t in b`. +Also, :g:`term :>` explicitly asks the system to coerce term to its support type. It can be useful in notations, for example: @@ -180,7 +189,7 @@ Program Definition Program Fixpoint ~~~~~~~~~~~~~~~~ -.. cmd:: Program Fixpoint @ident @params {? {@order}} : @type := @term +.. cmd:: Program Fixpoint @ident @binders {? {@order}} : @type := @term The optional order annotation follows the grammar: |