diff options
author | 2017-12-10 21:43:10 +0100 | |
---|---|---|
committer | 2017-12-12 13:30:58 +0100 | |
commit | 7720a01ceb7d00bc16cd96d99c27bc7696388899 (patch) | |
tree | 8a362dd6122c61a37846d8a883a783d2369b1029 /doc | |
parent | dd47b90184440eacafac0d98bbd3b24b57579df1 (diff) |
Documenting the new options for printing "match".
Namely:
- Set Printing Factorizable Match Patterns.
= Set Printing Allow Default Clause.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-ext.tex | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 5c519e46e..a1950d136 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -550,6 +550,60 @@ the same way as the {\Coq} kernel handles them. This tells if the printing matching mode is on or off. The default is on. +\subsubsection{Factorization of clauses with same right-hand side} +\label{SetPrintingFactorizableMatchPatterns} +\optindex{Printing Factorizable Match Patterns} + +When several patterns share the same right-hand side, it is +additionally possible to share the clauses using disjunctive patterns. +Assuming that the printing matching mode is on, whether {\Coq}'s +printer shall try to do this kind of factorization is governed by the +following commands: + +\begin{quote} +{\tt Set Printing Factorizable Match Patterns.} +\end{quote} +This tells {\Coq}'s printer to try to use disjunctive patterns. This is the default +behavior. + +\begin{quote} +{\tt Unset Printing Factorizable Match Patterns.} +\end{quote} +This tells {\Coq}'s printer not to try to use disjunctive patterns. + +\begin{quote} +{\tt Test Printing Factorizable Match Patterns.} +\end{quote} +This tells if the factorization of clauses with same right-hand side is +on or off. + +\subsubsection{Use of a default clause} +\label{SetPrintingAllowDefaultClause} +\optindex{Printing Allow Default Clause} + +When several patterns share the same right-hand side which do not +depend on the arguments of the patterns, yet an extra factorization is +possible: the disjunction of patterns can be replaced with a ``{\tt + \_}'' default clause. Assuming that the printing matching mode and +the factorization mode are on, whether {\Coq}'s printer shall try to +use a default clause is governed by the following commands: + +\begin{quote} +{\tt Set Printing Allow Default Clause.} +\end{quote} +This tells {\Coq}'s printer to use a default clause when relevant. This is the default +behavior. + +\begin{quote} +{\tt Unset Printing Allow Default Clause.} +\end{quote} +This tells {\Coq}'s printer not to use a default clause. + +\begin{quote} +{\tt Test Printing Allow Default Clause.} +\end{quote} +This tells if the use of a default clause is allowed. + \subsubsection{Printing of wildcard pattern \optindex{Printing Wildcard}} |