diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-12-14 17:22:07 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-14 17:22:07 +0100 |
commit | 84e570d7c532f16104157b806da714906fdf26b3 (patch) | |
tree | f020dcc0e2e599ae02d045240a076900595ea056 /doc/refman/RefMan-ext.tex | |
parent | 8f936f45ab95fdb72f1d596fc621faa39ddcb95e (diff) | |
parent | 7720a01ceb7d00bc16cd96d99c27bc7696388899 (diff) |
Merge PR #978: In printing, experimenting factorizing "match" clauses with same right-hand side.
Diffstat (limited to 'doc/refman/RefMan-ext.tex')
-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}} |